diff options
Diffstat (limited to 'stm/lemmas.ml')
| -rw-r--r-- | stm/lemmas.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index ce5ef0169..afbc407d8 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -150,7 +150,7 @@ let find_mutually_recursive_statements thms = assert (List.is_empty rest); (* One occ. of common coind ccls and no common inductive hyps *) if not (List.is_empty common_same_indhyp) then - if_verbose msg_info (str "Assuming mutual coinductive statements."); + if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements."); flush_all (); indccl, true, [] | [], _::_ -> @@ -158,7 +158,7 @@ let find_mutually_recursive_statements thms = | ind :: _ -> if List.distinct_f ind_ord (List.map pi1 ind) then - if_verbose msg_info + if_verbose Feedback.msg_info (strbrk ("Coinductive statements do not follow the order of "^ "definition, assuming the proof to be by induction.")); @@ -306,7 +306,7 @@ let admit (id,k,e) pl hook () = let () = match k with | Global, _, _ -> () | Local, _, _ | Discharge, _, _ -> - msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++ + Feedback.msg_warning (str "Let definition" ++ spc () ++ pr_id id ++ spc () ++ str "declared as an axiom.") in let () = assumption_message id in @@ -336,7 +336,7 @@ let universe_proof_terminator compute_guard hook = make_terminator begin function | Admitted (id,k,pe,(ctx,pl)) -> admit (id,k,pe) pl (hook (Some ctx)) (); - Pp.feedback Feedback.AddedAxiom + Feedback.feedback Feedback.AddedAxiom | Proved (opaque,idopt,proof) -> let is_opaque, export_seff, exports = match opaque with | Vernacexpr.Transparent -> false, true, [] |