Evarconv: Fix #2936 + comments

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

1 files changed, 13 insertions, 0 deletions

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))))).