diff options
| author | Maxime Dénès | 2016-07-03 18:54:06 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-07-03 18:54:06 +0200 |
| commit | e278d031a1d9a7bf3de463d3d415065299c99395 (patch) | |
| tree | ddd3a123e1887a9fa4634af7559bc7bb67b0cc25 /plugins/funind/invfun.ml | |
| parent | d7664c0530edd196d52e9fd8a4b925dbfefd1b9b (diff) | |
| parent | 3ce70f21a18cc19e720e8ac54b93652527881942 (diff) | |
Merge branch 'cerrors-cclosure' into trunk
Was PR#226: CErrors & CClosure
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 1ff254f6ca..26fc88a604 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 e = Cerrors.process_vernac_interp_error reraise in + let reraise = CErrors.push reraise in + let e = ExplainErr.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;; @@ -90,7 +90,7 @@ let observe_tac s tac g = (* [nf_zeta] $\zeta$-normalization of a term *) let nf_zeta = - Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) + Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) Environ.empty_env Evd.empty @@ -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 |