diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-26 02:12:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:43 +0100 |
| commit | c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 (patch) | |
| tree | f57eaac2d0c3cee82b172556eca53f16e0f0a900 /tactics/leminv.ml | |
| parent | 01849481fbabc3a3fa6c483e703996b01e37fca5 (diff) | |
Evar-normalizing functions now act on EConstrs.
Diffstat (limited to 'tactics/leminv.ml')
| -rw-r--r-- | tactics/leminv.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 3199623e7..a05b4fbf3 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -208,14 +208,12 @@ let inversion_scheme env sigma t sort dep_option inv_op = user_err ~hdr:"lemma_inversion" (str"Computed inversion goal was not closed in initial signature."); *) - let invGoal = EConstr.Unsafe.to_constr invGoal in let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in let pf = fst (Proof.run_tactic env ( tclTHEN intro (onLastHypId inv_op)) pf) in let pfterm = List.hd (Proof.partial_proof pf) in - let pfterm = EConstr.of_constr pfterm in let global_named_context = Global.named_context_val () in let ownSign = ref begin fold_named_context |