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

2 files changed, 28 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
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index ad69ced19e..26e62ae622 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -74,3 +74,15 @@ eauto.
 
 Check (exist _ O (refl_equal 0) : {n:nat|n=0}).
 Check (exist _ O I : {n:nat|True}).
+
+(* An example (initially from Marseille/Fairisle) that involves an evar with
+   different solutions (Input, Output or bool) that may or may not be
+   considered distinct depending on which kind of conversion is used *)
+
+Section A.
+Definition STATE := (nat * bool)%type.
+Let Input := bool.
+Let Output := bool.
+Parameter Out : STATE -> Output.
+Check fun (s : STATE) (reg : Input) => reg = Out s.
+End A.