From e2655d38d11b072da0e5f4d40b05adbea73c8b8d Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 10 Apr 2009 19:23:58 +0000
Subject: Fix premature optimisation in dependent induction: even variable args
 need to be generalized as they may appear in other arguments or their types.
 Try to keep the original names around as well, using the ones found in the
 goal. This only requires that interning a pattern [forall x, _] properly
 declares [x] as a metavariable, binding instances are already part of the
 substitutions computed by [extended_matches].

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12079 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index fa0dd6e0c4..9940f04b5a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2173,8 +2173,8 @@ let abstract_args gl id =
 	  let liftargty = lift (List.length ctx) argty in
 	  let convertible = Reductionops.is_conv_leq ctxenv sigma liftargty ty in
 	    match kind_of_term arg with
-	    | Var _ | Rel _ | Ind _ when convertible -> 
-		(subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, vars, env)
+(* 	    | Var _ | Rel _ | Ind _ when convertible ->  *)
+(* 		(subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, vars, env) *)
 	    | _ ->
 		let name = get_id name in
 		let decl = (Name name, None, ty) in
-- 
cgit v1.2.3