diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-27 11:03:43 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-07-03 12:08:03 +0200 |
commit | f14b6f1a17652566f0cbc00ce81421ba0684dad5 (patch) | |
tree | 8a331593d0d1b518e8764c92ac54e3b11c222358 /stm/lemmas.ml | |
parent | 500d38d0887febb614ddcadebaef81e0c7942584 (diff) |
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
Diffstat (limited to 'stm/lemmas.ml')
-rw-r--r-- | stm/lemmas.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 404e10427..fb2f0351d 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -9,7 +9,7 @@ (* Created by Hugo Herbelin from contents related to lemma proofs in file command.ml, Aug 2009 *) -open Errors +open CErrors open Util open Flags open Pp @@ -37,8 +37,8 @@ type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> let mk_hook hook = hook let call_hook fix_exn hook l c = try hook l c - with e when Errors.noncritical e -> - let e = Errors.push e in + with e when CErrors.noncritical e -> + let e = CErrors.push e in iraise (fix_exn e) (* Support for mutually proved theorems *) @@ -210,8 +210,8 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook = definition_message id; Option.iter (Universes.register_universe_binders r) pl; call_hook (fun exn -> exn) hook l r - with e when Errors.noncritical e -> - let e = Errors.push e in + with e when CErrors.noncritical e -> + let e = CErrors.push e in iraise (fix_exn e) let default_thm_id = Id.of_string "Unnamed_thm" |