diff options
Diffstat (limited to 'vernac/lemmas.ml')
| -rw-r--r-- | vernac/lemmas.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 391e78bcd..4b36c2d07 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -11,7 +11,6 @@ open CErrors open Util -open Flags open Pp open Names open Term @@ -137,7 +136,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 Feedback.msg_info (str "Assuming mutual coinductive statements."); + Flags.if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements."); flush_all (); indccl, true, [] | [], _::_ -> @@ -145,7 +144,7 @@ let find_mutually_recursive_statements thms = | ind :: _ -> if List.distinct_f ind_ord (List.map pi1 ind) then - if_verbose Feedback.msg_info + Flags.if_verbose Feedback.msg_info (strbrk ("Coinductive statements do not follow the order of "^ "definition, assuming the proof to be by induction.")); |