From f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 6 Aug 2010 16:15:08 -0400
Subject: Imported Upstream version 8.3~rc1+dfsg

---
 tactics/tactics.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'tactics/tactics.ml')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e09707ab..9e4be0af 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: tactics.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Pp
 open Util
@@ -2320,6 +2320,9 @@ let linear vars args =
       true
     with Seen -> false
 
+let is_defined_variable env id =
+  pi2 (lookup_named id env) <> None
+
 let abstract_args gl generalize_vars dep id defined f args =
   let sigma = project gl in
   let env = pf_env gl in
@@ -2347,7 +2350,7 @@ let abstract_args gl generalize_vars dep id defined f args =
     let liftargty = lift lenctx argty in
     let leq = constr_cmp Reduction.CUMUL liftargty ty in
       match kind_of_term arg with
-      | Var id when leq && not (Idset.mem id nongenvars) ->
+      | Var id when not (is_defined_variable env id) && leq && not (Idset.mem id nongenvars) ->
       	  (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls,
       	  Idset.add id nongenvars, Idset.remove id vars, env)
       | _ ->
@@ -2374,7 +2377,7 @@ let abstract_args gl generalize_vars dep id defined f args =
     let parvars = ids_of_constr ~all:true Idset.empty f' in
       if not (linear parvars args') then true, f, args
       else
-	match array_find_i (fun i x -> not (isVar x)) args' with
+	match array_find_i (fun i x -> not (isVar x) || is_defined_variable env (destVar x)) args' with
 	| None -> false, f', args'
 	| Some nonvar ->
 	    let before, after = array_chop nonvar args' in
-- 
cgit v1.2.3