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). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- contrib/correctness/pcicenv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'contrib/correctness') diff --git a/contrib/correctness/pcicenv.ml b/contrib/correctness/pcicenv.ml index c9c0ed4b2..4ac4e9704 100644 --- a/contrib/correctness/pcicenv.ml +++ b/contrib/correctness/pcicenv.ml @@ -38,7 +38,7 @@ let add_sign (id,t) s = let cast_set c = mkCast (c, mkSet) -let set = mkCast (mkSet, mkType Univ.prop_univ) +let set = mkCast (mkSet, mkType Univ.type1_univ) (* [cci_sign_of env] construit un environnement pour CIC ne comprenant que * les objets fonctionnels de l'environnement de programes [env] -- cgit v1.2.3