Evarconv: Fix #2936 + comments

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

2 files changed, 37 insertions, 9 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 42dd7201d..5303252c8 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -143,8 +143,12 @@ let ise_and evd l =
         if b then  ise_and i' l else (evd,false) in
   ise_and evd l
 
-(* This function requires to get the outermost arguments first.
-   It is a fold_right to be backward compatibility.
+(* This function requires to get the outermost arguments first.  It is
+   a fold_right for backward compatibility.
+
+   It tries to unify the suffix of 2 lists element by element and if
+   it reaches the end of a list, it returns the remaining elements in
+   the other list if there are some.
 *)
 let generic_ise_list2 i f l1 l2 =
   let rec aux i l1 l2 =
@@ -157,6 +161,7 @@ let generic_ise_list2 i f l1 l2 =
       if b then (aa, f i' x y) else None, (i, false)
   in aux i (List.rev l1) (List.rev l2)
 
+(* Same but the 2 lists must have the same length *)
 let ise_list2 evd f l1 l2 =
   match generic_ise_list2 evd f l1 l2 with
   | None, out -> out
@@ -173,6 +178,10 @@ let ise_array2 evd f v1 v2 =
   if Int.equal lv1 (Array.length v2) then allrec evd (pred lv1)
   else (evd,false)
 
+(* This function tries to unify 2 stacks element by element. It works
+   from the end to the beginning. If it unifies a non empty suffix of
+   stacks but not the entire stacks, the first part of the answer is
+   Some(the remaining prefixes to tackle)) *)
 let ise_stack2 no_app env evd f sk1 sk2 =
   let rec ise_stack2 deep i sk1 sk2 =
     let fal () = if deep then Some (List.rev sk1, List.rev sk2), (i,deep)
@@ -196,6 +205,11 @@ let ise_stack2 no_app env evd f sk1 sk2 =
     | Zupdate _ :: _, _ | Zshift _ :: _, _
     | _, Zupdate _ :: _ | _, Zshift _ :: _ -> assert false
     | Zapp l1 :: q1, Zapp l2 :: q2 -> if no_app&&deep then fal () else begin
+      (* Is requiring to match on all the shorter list a restriction
+	 here ? we could imagine a generalization of
+	 generic_ise_list2 that succeed when it matches only a strict
+	 non empty suffix of both lists and returns in this case the 2
+	 prefixes *)
       match generic_ise_list2 i (fun ii -> f env ii CONV) l1 l2 with
       |_,(_, false) -> fal ()
       |None,(i', true) -> ise_stack2 true i' q1 q2
@@ -205,6 +219,7 @@ let ise_stack2 no_app env evd f sk1 sk2 =
     |_, _ -> fal ()
   in ise_stack2 false evd (List.rev sk1) (List.rev sk2)
 
+(* Make sure that the matching suffix is the all stack *)
 let exact_ise_stack2 env evd f sk1 sk2 =
   match ise_stack2 false env evd f sk1 sk2 with | None, out -> out | _ -> (evd, false)
 
@@ -425,7 +440,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
         let c = nf_evar evd c1 in
 	let env' = push_rel (na,None,c) env in
         let appr1 = whd_betaiota_deltazeta_for_iota_state  ts env' evd (c'1, empty_stack) in
-	let appr2 = (term2, sk2 @ [Zshift 1 ; Zapp [mkRel 1]]) in
+	let appr2 = whd_nored_state evd (zip (term2, sk2 @ [Zshift 1]), [Zapp [mkRel 1]]) in
 	evar_eqappr_x ts env' evd CONV appr1 appr2
 
     | _, Rigid when isLambda term2 ->
@@ -433,7 +448,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
 	let (na,c2,c'2) = destLambda term2 in
         let c = nf_evar evd c2 in
 	let env' = push_rel (na,None,c) env in
-	let appr1 = (term1, sk1 @ [Zshift 1 ; Zapp [mkRel 1]]) in
+	let appr1 = whd_nored_state evd (zip (term1, sk1 @ [Zshift 1]), [Zapp [mkRel 1]]) in
         let appr2 = whd_betaiota_deltazeta_for_iota_state ts env' evd (c'2, empty_stack) in
 	evar_eqappr_x ts env' evd CONV appr1 appr2
 
@@ -441,11 +456,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
         match kind_of_term term1, kind_of_term term2 with
 
 	| Sort s1, Sort s2 when app_empty ->
-	    (try 
-	       let evd' = 
-		 if pbty == CONV 
-		 then Evd.set_eq_sort evd s1 s2 
-		 else Evd.set_leq_sort evd s1 s2 
+	    (try
+	       let evd' =
+		 if pbty == CONV
+		 then Evd.set_eq_sort evd s1 s2
+		 else Evd.set_leq_sort evd s1 s2
 	       in (evd', true)
 	     with Univ.UniverseInconsistency _ -> (evd, false)
 	     | _ -> (evd, false))
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index ceb940a45..ff8b28bae 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -1,3 +1,4 @@
+
 (* The "?" of cons and eq should be inferred *)
 Variable list : Set -> Set.
 Variable cons : forall T : Set, T -> list T -> list T.
@@ -379,3 +380,15 @@ Section evar_evar_occur.
   (* Still evars in the resulting type, but constraints should be solved *)
   Check match g _ with conj a b => f _ a b end.
 End evar_evar_occur.
+
+(* Eta expansion (bug #2936) *)
+Record iffT (X Y:Type) : Type := mkIff { iffLR : X->Y; iffRL : Y->X }.
+Record tri (R:Type->Type->Type) (S:Type->Type->Type) (T:Type->Type->Type) := mkTri {
+  tri0 : forall a b c, R a b -> S a c -> T b c
+}.
+Implicit Arguments mkTri [R S T].
+Definition tri_iffT : tri iffT iffT iffT :=
+  (mkTri
+    (fun X0 X1 X2 E01 E02 =>
+     (mkIff _ _ (fun x1 => iffLR _ _ E02 (iffRL _ _ E01 x1))
+     (fun x2 => iffLR _ _ E01 (iffRL _ _ E02 x2))))).