From 31c44227059be9227f8fc921f74a80094f9bbcfe Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 8 Apr 2011 14:08:50 +0000
Subject: 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
---
 pretyping/coercion.ml                   |  2 +-
 test-suite/failure/universes2.v         |  4 ----
 test-suite/success/universes-coercion.v | 22 ++++++++++++++++++++++
 3 files changed, 23 insertions(+), 5 deletions(-)
 delete mode 100644 test-suite/failure/universes2.v
 create mode 100644 test-suite/success/universes-coercion.v

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 5503a147a6..389761aeb9 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 e74de70fc8..0000000000
--- 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 0000000000..d750434027
--- /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"
+*)
-- 
cgit v1.2.3