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 /plugins/funind/invfun.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 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 1ff254f6c..ad5d077d6 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -8,7 +8,7 @@ open Tacexpr open Declarations -open Errors +open CErrors open Util open Names open Term @@ -65,16 +65,16 @@ let observe strm = let do_observe_tac s tac g = let goal = try Printer.pr_goal g - with e when Errors.noncritical e -> assert false + with e when CErrors.noncritical e -> assert false in try let v = tac g in msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v with reraise -> - let reraise = Errors.push reraise in + let reraise = CErrors.push reraise in let e = Cerrors.process_vernac_interp_error reraise in observe (hov 0 (str "observation "++ s++str " raised exception " ++ - Errors.iprint e ++ str " on goal" ++ fnl() ++ goal )); + CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal )); iraise reraise;; @@ -585,7 +585,7 @@ let rec reflexivity_with_destruct_cases g = observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases ] | _ -> Proofview.V82.of_tactic reflexivity - with e when Errors.noncritical e -> Proofview.V82.of_tactic reflexivity + with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity in let eq_ind = make_eq () in let discr_inject = @@ -998,7 +998,7 @@ let invfun qhyp f = let f = match f with | ConstRef f -> f - | _ -> raise (Errors.UserError("",str "Not a function")) + | _ -> raise (CErrors.UserError("",str "Not a function")) in try let finfos = find_Function_infos f in |