Réponse à une incompatibilité introduite dans 10114 (calcul du nombre

de solutions distinctes faites modulo égalité d'alias uniquement et pas
modulo toute la puissance de la convertibilité)


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

1 files changed, 16 insertions, 1 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 28473962a8..79d4467d8e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -436,6 +436,20 @@ and clear_hyps_in_evi evdref evi ids =
 
 let need_restriction k args = not (array_for_all (closedn k) args)
 
+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
+
 (* [find_projectable_vars env sigma y subst] finds all vars of [subst]
  * that project on [y] up to variables aliasing.  In case of solutions that
  * differ only up to aliasing, the binding that requires the less
@@ -465,7 +479,8 @@ type evar_projection =
 
 let rec find_projectable_vars env sigma y subst =
   let is_projectable (id,(idc,y')) =
-    if is_conv env sigma y y' then (idc,(y'=y,(id,ProjectVar)))
+    if y = y' or expand_var env y = expand_var env y'
+    then (idc,(y'=y,(id,ProjectVar)))
     else if isEvar y' then
       let (evk,argsv as t) = destEvar y' in
       let evi = Evd.find sigma evk in