From 32a26cd2dde0f9c31fec6952c830eb09bfb260d8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 9 Jun 2008 11:26:32 +0000
Subject: - Documentation de admit et Print Assumptions. - Relecture, mise à
 jour, correction d'erreurs et petite   réorganisation du chapitre sur les
 commandes vernaculaires. - Correction bug #1865 (rafraichissement des univers
 algébriques). - Suppression de la dépendance du initial.coq en les noms longs
 des fichiers   de façons à ce que les dépendances ne soient que purement
 logique. - Encore un (petit) bug undo ide.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11077 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/retyping.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 795627fc41..8b32224d2d 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -92,10 +92,12 @@ let retype sigma metamap =
           | Prop _, (Prop Pos as s) -> s
           | Type _, (Prop Pos as s) when
               Environ.engagement env = Some ImpredicativeSet -> s
+	  | (Type _, _) | (_, Type _) -> new_Type_sort ()
+(*
           | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.type0_univ)
 	  | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2)
 	  | Prop Null, (Type _ as s) -> s
-	  | Type u1, Type u2 -> Type (Univ.sup u1 u2))
+	  | Type u1, Type u2 -> Type (Univ.sup u1 u2)*))
     | App(f,args) when isGlobalRef f ->
 	let t = type_of_global_reference_knowing_parameters env f args in
         sort_of_atomic_type env sigma t args
-- 
cgit v1.2.3