diff options
| author | Pierre-Marie Pédrot | 2020-08-31 13:06:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-09-02 19:06:33 +0200 |
| commit | c36fd380fb6b04ef23cb61bd4f792bdd2c472725 (patch) | |
| tree | 03d95095d86ff68f502d2d3174cd0abe4e9baa04 | |
| parent | 7628e20be2b2e02dee595a69c62de04a68c2d36f (diff) | |
Remove the opening of CErrors in Elim.
| -rw-r--r-- | tactics/elim.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index 0556d2717d..852ad626e1 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open CErrors open Util open Names open Constr @@ -48,7 +47,7 @@ let general_elim_then_using mk_elim let indmv = match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with | Meta mv -> mv - | _ -> anomaly (str"elimination.") + | _ -> CErrors.anomaly (str"elimination.") in let pmv = let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in @@ -60,7 +59,7 @@ let general_elim_then_using mk_elim | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim | _ -> mt () in - user_err ~hdr:"Tacticals.general_elim_then_using" + CErrors.user_err ~hdr:"Tacticals.general_elim_then_using" (str "The elimination combinator " ++ name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in @@ -108,7 +107,7 @@ end let make_elim_branch_assumptions ba hyps = let assums = try List.rev (List.firstn ba.nassums hyps) - with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions.") in + with Failure _ -> CErrors.anomaly (Pp.str "make_elim_branch_assumptions.") in assums let elim_on_ba tac ba = |