diff options
| author |  Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 17:47:10 +0200 |
| commit | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (patch) | |
| tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /toplevel/indschemes.ml | |
| parent | bf12eb93f3f6a6a824a10878878fadd59745aae0 (diff) | |
Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg
Diffstat (limited to 'toplevel/indschemes.ml')
| -rw-r--r-- | toplevel/indschemes.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index fa6885af..e30404e1 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -159,7 +159,7 @@ let try_declare_scheme what f internal names kn = (strbrk "Required constant " ++ str s ++ str " undefined.") | AlreadyDeclared msg -> alarm what internal (msg ++ str ".") - | _ -> + | e when Errors.noncritical e -> alarm what internal (str "Unknown exception during scheme creation.") @@ -245,7 +245,8 @@ 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 _ -> () +let ignore_error f x = + try ignore (f x) with e when Errors.noncritical e -> () let declare_rewriting_schemes ind = if Hipattern.is_inductive_equality ind then begin @@ -266,7 +267,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 _ -> false + with e when Errors.noncritical e -> false then ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind) else |