diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-19 18:18:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-19 18:18:34 +0200 |
| commit | c7dcb76ffff6b12b031e906b002b4d76c1aaea50 (patch) | |
| tree | 8d5115258c3b7042767e45d742e2800dab209822 /proofs | |
| parent | 666568377cbe1c18ce479d32f6359aa61af6d553 (diff) | |
| parent | 50a574f8b3e7f29550d7abf600d92eb43e7f8ef6 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof_global.mli | 2 | ||||
| -rw-r--r-- | proofs/tactic_debug.ml | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index a11c7b4e0..929bb86e8 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -97,7 +97,7 @@ val start_dependent_proof : val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof (* Intermediate step necessary to delegate the future. - * Both access the current proof state. The formes is supposed to be + * Both access the current proof state. The former is supposed to be * chained with a computation that completed the proof *) type closed_proof_output = (Term.constr * Declareops.side_effects) list * Evd.evar_universe_context diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 667765dbf..6d6215c52 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -33,7 +33,7 @@ let explain_logic_error = ref (fun e -> mt()) let explain_logic_error_no_anomaly = ref (fun e -> mt()) let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl()) -let msg_tac_notice s = Proofview.NonLogical.print (s++fnl()) +let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl()) (* Prints the goal *) @@ -122,7 +122,7 @@ let run ini = let open Proofview.NonLogical in if not ini then begin - Proofview.NonLogical.print (str"\b\r\b\r") >> + Proofview.NonLogical.print_notice (str"\b\r\b\r") >> !skipped >>= fun skipped -> msg_tac_debug (str "Executed expressions: " ++ int skipped ++ fnl()) end >> @@ -137,7 +137,7 @@ let rec prompt level = let runtrue = run true in begin let open Proofview.NonLogical in - Proofview.NonLogical.print (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> + Proofview.NonLogical.print_notice (fnl () ++ str "TcDebug (" ++ int level ++ str ") > ") >> let exit = (skip:=0) >> (skipped:=0) >> raise Sys.Break in Proofview.NonLogical.catch Proofview.NonLogical.read_line begin function (e, info) -> match e with |