Applying and reworking Tom Prince's patch for test-suite/failure/universes2.v

which did not test what it was supposed to test

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

3 files changed, 23 insertions, 5 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 5503a147a..389761aeb 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -202,7 +202,7 @@ module Default = struct
         (* We eta-expand (hence possibly modifying the original term!) *)
 	(* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *)
 	(* has type forall (x:u1), u2 (with v' recursively obtained) *)
-        (* Note: we retupe the term because sort-polymorphism may have *)
+        (* Note: we retype the term because sort-polymorphism may have *)
         (* weaken its type *)
 	let name = match name with
 	  | Anonymous -> Name (id_of_string "x")
diff --git a/test-suite/failure/universes2.v b/test-suite/failure/universes2.v
deleted file mode 100644
index e74de70fc..000000000
--- a/test-suite/failure/universes2.v
+++ /dev/null
@@ -1,4 +0,0 @@
-(* Example submitted by Randy Pollack *)
-
-Parameter K : forall T : Type, T -> T.
-Check (K (forall T : Type, T -> T) K).
diff --git a/test-suite/success/universes-coercion.v b/test-suite/success/universes-coercion.v
new file mode 100644
index 000000000..d75043402
--- /dev/null
+++ b/test-suite/success/universes-coercion.v
@@ -0,0 +1,22 @@
+(* This example used to emphasize the absence of LEGO-style universe
+   polymorphism; Matthieu's improvements of typing on 2011/3/11 now
+   makes (apparently) that Amokrane's automatic eta-expansion in the
+   coercion mechanism works; this makes its illustration as a "weakness"
+   of universe polymorphism obsolete (example submitted by Randy Pollack).
+
+   Note that this example is not an evidence that the current
+   non-kernel eta-expansion behavior is the most expected one.  
+*)
+
+Parameter K : forall T : Type, T -> T.
+Check (K (forall T : Type, T -> T) K).
+
+(*
+   note that the inferred term is
+     "(K (forall T (* u1 *) : Type, T -> T) (fun T:Type (* u1 *) => K T))"
+   which is not eta-equivalent to 
+     "(K (forall T : Type, T -> T) K"
+   because the eta-expansion of the latter
+     "(K (forall T : Type, T -> T) (fun T:Type (* u2 *) => K T)"
+  assuming K of type "forall T (* u2 *) : Type, T -> T"
+*)