diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-25 11:36:09 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:39 +0100 |
| commit | 778e863b77bcafc8ed339dd02226e85e5fee2532 (patch) | |
| tree | c836854265a6c1ac401b524710a0b7947bea3d37 /tactics/leminv.ml | |
| parent | 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 (diff) | |
Removing compatibility layers related to printing.
Diffstat (limited to 'tactics/leminv.ml')
| -rw-r--r-- | tactics/leminv.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index ef3bfc9d0..2d59285e6 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -42,7 +42,7 @@ let nlocal_def (na, b, t) = let no_inductive_inconstr env sigma constr = (str "Cannot recognize an inductive predicate in " ++ - pr_lconstr_env env sigma (EConstr.Unsafe.to_constr constr) ++ + pr_leconstr_env env sigma constr ++ str "." ++ spc () ++ str "If there is one, may be the structure of the arity" ++ spc () ++ str "or of the type of constructors" ++ spc () ++ str "is hidden by constant definitions.") @@ -277,14 +277,12 @@ let lemInv id c gls = Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls with | NoSuchBinding -> - let c = EConstr.Unsafe.to_constr c in user_err - (hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma.")) + (hov 0 (pr_econstr_env (Refiner.pf_env gls) (Refiner.project gls) c ++ spc () ++ str "does not refer to an inversion lemma.")) | UserError (a,b) -> - let c = EConstr.Unsafe.to_constr c in user_err ~hdr:"LemInv" (str "Cannot refine current goal with the lemma " ++ - pr_lconstr_env (Refiner.pf_env gls) (Refiner.project gls) c) + pr_leconstr_env (Refiner.pf_env gls) (Refiner.project gls) c) let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id |