From ca3812d7804f3936bb420e96fad034983ede271a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 27 Apr 2008 16:46:15 +0000
Subject: Correction du bug des types singletons pas sous-type de Set (i.e.
 "Inductive unit := tt." conduisait à "t:Prop" alors que le principe de la
 hiérarchie d'univers est d'être cumulative -- et que Set en soit le niveau
 0).

Une solution aurait été de poser Prop <= Set mais on adopte une autre
solution. Pour éviter le côté contre-intuitif d'avoir unit dans Type
et Prop <= Set, on garde la représentation de Prop au sein de la
hiérarchie prédicative sous la forme "Type (max ([],[])" (le niveau
sans aucune contrainte inférieure, appelons Type -1) et on adapte les
fonctions de sous-typage et de typage pour qu'elle prenne en compte la
règle Type -1 <= Prop (cf reduction.ml, reductionops.ml, et effets
incidents dans Termops.refresh_universes et Univ.super).

Petite uniformisation des noms d'univers et de sortes au passage
(univ.ml, univ.mli, term.ml, term.mli et les autres fichiers).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10859 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/typeops.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index a09b0799b8..616349ba0a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -59,11 +59,11 @@ let sort_judgment env j = (type_judgment env j).utj_type
 
 let judge_of_prop =
   { uj_val = mkProp;
-    uj_type = mkSort type_0 }
+    uj_type = mkSort type1_sort }
 
 let judge_of_set =
   { uj_val = mkSet;
-    uj_type = mkSort type_0 }
+    uj_type = mkSort type1_sort }
 
 let judge_of_prop_contents = function
   | Null -> judge_of_prop
@@ -237,9 +237,9 @@ let sort_of_product env domsort rangsort =
           rangsort
         else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
-          Type (sup u1 base_univ)
+          Type (sup u1 type0_univ)
     (* Product rule (Prop,Type_i,Type_i) *)
-    | (Prop Pos,  Type u2)  -> Type (sup base_univ u2)
+    | (Prop Pos,  Type u2)  -> Type (sup type0_univ u2)
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Null, Type _)  -> rangsort
     (* Product rule (Type_i,Type_i,Type_i) *) 
-- 
cgit v1.2.3