From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- tactics/leminv.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics/leminv.ml') 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 -- cgit v1.2.3