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 60d05ec70..481b78683 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -216,7 +216,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 invSign = named_context invEnv in + let invSign = named_context_val invEnv in let pfs = mk_pftreestate (mk_goal invSign invGoal) in let pfs = solve_pftreestate (tclTHEN intro (onLastHyp inv_op)) pfs in let (pfterm,meta_types) = extract_open_pftreestate pfs in |