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/term.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index 70c5ceded9..9254a6ff83 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -21,9 +21,9 @@ type sorts =
   | Prop of contents       (* Prop and Set *)
   | Type of Univ.universe  (* Type *)
 
-val mk_Set  : sorts
-val mk_Prop : sorts
-val type_0  : sorts
+val set_sort  : sorts
+val prop_sort : sorts
+val type1_sort  : sorts
 
 (*s The sorts family of CCI. *)
 
-- 
cgit v1.2.3