Skip to content

Commit

Permalink
Use CDebug instead of msg_debug in indschemes
Browse files Browse the repository at this point in the history
This allows enabling the debug without having to recompile to switch
the static `let debug = false`.
  • Loading branch information
SkySkimmer committed Oct 26, 2023
1 parent 08dcbc5 commit fc4076e
Showing 1 changed file with 5 additions and 4 deletions.
9 changes: 5 additions & 4 deletions vernac/indschemes.ml
Original file line number Diff line number Diff line change
Expand Up @@ -107,13 +107,14 @@ let define ~poly name sigma c types =
let declare_beq_scheme_gen ?locmap names kn =
ignore (define_mutual_scheme ?locmap beq_scheme_kind names kn)

let debug = CDebug.create ~name:"indschemes" ()

let alarm what internal msg =
let debug = false in
match internal with
| UserAutomaticRequest ->
(if debug then
Feedback.msg_debug
(hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None
debug Pp.(fun () ->
hov 0 msg ++ fnl () ++ what ++ str " not defined.");
None
| UserIndividualRequest -> Some msg

let try_declare_scheme ?locmap what f internal names kn =
Expand Down

0 comments on commit fc4076e

Please sign in to comment.