diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
| commit | 70b9be8acc1d1ada178a95c1cd4013506e9d0d1b (patch) | |
| tree | f672a286d962cc67c95874b3b60402fc957870b6 /tactics/leminv.ml | |
| parent | a5bd4e097a94cc4f863bf4d4bcc5ce592c30ba47 (diff) | |
| parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) | |
Merge commit 'upstream/8.1.gamma' into 8.1
Diffstat (limited to 'tactics/leminv.ml')
| -rw-r--r-- | tactics/leminv.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 7974ce56..9507ce5f 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: leminv.ml 7837 2006-01-11 09:47:32Z herbelin $ *) +(* $Id: leminv.ml 9154 2006-09-20 17:18:18Z corbinea $ *) open Pp open Util @@ -217,7 +217,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = (str"Computed inversion goal was not closed in initial signature"); *) let invSign = named_context_val invEnv in - let pfs = mk_pftreestate (mk_goal invSign invGoal) in + let pfs = mk_pftreestate (mk_goal invSign invGoal None) in let pfs = solve_pftreestate (tclTHEN intro (onLastHyp inv_op)) pfs in let (pfterm,meta_types) = extract_open_pftreestate pfs in let global_named_context = Global.named_context () in |