diff options
Diffstat (limited to 'toplevel/indschemes.ml')
| -rw-r--r-- | toplevel/indschemes.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index bbee39c3d..32e0eb53b 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -15,7 +15,7 @@ declaring new schemes *) open Pp -open Errors +open CErrors open Util open Names open Declarations @@ -157,7 +157,7 @@ let alarm what internal msg = let try_declare_scheme what f internal names kn = try f internal names kn with e -> - let e = Errors.push e in + let e = CErrors.push e in let msg = match fst e with | ParameterWithoutEquality cst -> alarm what internal @@ -186,9 +186,9 @@ let try_declare_scheme what f internal names kn = | DecidabilityMutualNotSupported -> alarm what internal (str "Decidability lemma for mutual inductive types not supported.") - | e when Errors.noncritical e -> + | e when CErrors.noncritical e -> alarm what internal - (str "Unexpected error during scheme creation: " ++ Errors.print e) + (str "Unexpected error during scheme creation: " ++ CErrors.print e) | _ -> iraise e in match msg with @@ -278,7 +278,7 @@ let try_declare_eq_decidability kn = let declare_eq_decidability = declare_eq_decidability_scheme_with [] let ignore_error f x = - try ignore (f x) with e when Errors.noncritical e -> () + try ignore (f x) with e when CErrors.noncritical e -> () let declare_rewriting_schemes ind = if Hipattern.is_inductive_equality ind then begin @@ -304,7 +304,7 @@ let declare_congr_scheme ind = if Hipattern.is_equality_type (mkInd ind) then begin if try Coqlib.check_required_library Coqlib.logic_module_name; true - with e when Errors.noncritical e -> false + with e when CErrors.noncritical e -> false then ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind) else |