diff options
Diffstat (limited to 'tactics/leminv.ml')
| -rw-r--r-- | tactics/leminv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 86ec3a8357..106205552d 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -196,7 +196,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = errorlabstrm "lemma_inversion" (str"Computed inversion goal was not closed in initial signature."); *) - let pf = Proof.start [invEnv,invGoal] in + let pf = Proof.start Evd.empty [invEnv,invGoal] in let pf = fst (Proof.run_tactic env ( Tacticals.New.tclTHEN intro (Tacticals.New.onLastHypId inv_op)) pf) |