Prise en compte des redéfinitions de variables (définitions locales

triviales en provenance de l'algo de compilation du filtrage) lors du
calcul de la projection des variables dans real_clean



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10103 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 2 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 5729d6c712..72f5fbf453 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -397,6 +397,23 @@ and clear_hyps_in_evi evd evi ids =
 
 let need_restriction k args = not (array_for_all (closedn k) args)
 
+(* A utility to circumvent the introduction of aliases to rel by the
+   pattern-matching compilation algorithm *)
+
+let rec expand_var env x = match kind_of_term x with
+  | Rel n -> 
+      begin try match pi2 (lookup_rel n env) with
+      | Some t when isRel t -> expand_var env (lift n t)
+      | _ -> x
+      with Not_found -> x
+      end
+  | Var id -> 
+      begin match pi2 (lookup_named id env) with
+      | Some t when isVar t -> expand_var env t
+      | _ -> x
+      end
+  | _ -> x
+
 (* We try to instantiate the evar assuming the body won't depend
  * on arguments that are not Rels or Vars, or appearing several times
  * (i.e. we tackle only Miller-Pfenning patterns unification) 
@@ -424,14 +441,15 @@ exception NotClean of constr
 
 let rec real_clean env isevars ev subst rhs =
   let evd = ref isevars in
-  let subst' = List.map (fun (x,y) -> (y,mkVar x)) subst in
+  let invert_binding (x,y) = (expand_var env y,mkVar x) in
+  let subst' = List.map invert_binding subst in
   let rec subs rigid k t =
     match kind_of_term t with
       | Rel i ->
  	 if i<=k then t
  	 else
 	   (* Flex/Rel problem: unifiable as a pattern iff Rel in ev scope *)
-	   (try List.assoc (mkRel (i-k)) subst' 
+	   (try List.assoc (expand_var env (mkRel (i-k))) subst' 
 	    with Not_found ->
 	      if rigid then
 		try unique_projection env evd (mkRel (i-k)) subst