From 0fcf7621f45a20765dbc7e39973abe78610dca64 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 27 Jun 2006 21:29:18 +0000
Subject: Correction bug #1182 (ajout refresh_universe car le polymorphisme de
 sorte des inductifs maintenant retourne des sortes d'inductives qui ne sont
 pas des variables) et test de non-régression

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8992 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/pretyping.ml      | 1 +
 test-suite/success/Case19.v | 8 ++++++++
 2 files changed, 9 insertions(+)
 create mode 100644 test-suite/success/Case19.v

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index be24d22b59..8b41b9c9b5 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -482,6 +482,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		       else
 			 error_cant_find_case_type_loc loc env (evars_of !isevars) 
 			   cj.uj_val in
+		     let ccl = refresh_universes ccl in
 		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
 		     let v =
 		       let mis,_ = dest_ind_family indf in
diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v
new file mode 100644
index 0000000000..9a6ed71a54
--- /dev/null
+++ b/test-suite/success/Case19.v
@@ -0,0 +1,8 @@
+(* This used to fail in Coq version 8.1 beta due to a non variable
+   universe (issued by the inductive sort-polymorphism) being sent by
+   pretyping to the kernel (bug #1182) *)
+
+Variable T : Type.
+Variable x : nat*nat.
+
+Check let (_, _) := x in sigT (fun _ : T => nat).
-- 
cgit v1.2.3