diff options
| author | herbelin | 2008-04-27 16:46:15 +0000 |
|---|---|---|
| committer | herbelin | 2008-04-27 16:46:15 +0000 |
| commit | ca3812d7804f3936bb420e96fad034983ede271a (patch) | |
| tree | 2e22e79f2225fcf3b7afcc29f99e844bd2460328 /kernel/subtyping.ml | |
| parent | d7e7e6756b46998e864cc00355d1946b69a43c1a (diff) | |
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
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 0c31d7962e..f5b3e87bdf 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -112,7 +112,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = let (ctx2,s2) = dest_arity env t2 in let s1,s2 = match s1, s2 with - | Type _, Type _ -> (* shortcut here *) mk_Prop, mk_Prop + | Type _, Type _ -> (* shortcut here *) prop_sort, prop_sort | (Prop _, Type _) | (Type _,Prop _) -> error () | _ -> (s1, s2) in check_conv cst conv_leq env @@ -222,13 +222,13 @@ let check_constant cst env msid1 l info1 cb2 spec2 = | Type u when not (is_univ_variable u) -> (* Both types are inferred, no need to recheck them. We cheat and collapse the types to Prop *) - Sign.mkArity (ctx1,mk_Prop), Sign.mkArity (ctx2,mk_Prop) + Sign.mkArity (ctx1,prop_sort), Sign.mkArity (ctx2,prop_sort) | Prop _ -> (* The type in the interface is inferred, it may be the case that the type in the implementation is smaller because the body is more reduced. We safely collapse the upper type to Prop *) - Sign.mkArity (ctx1,mk_Prop), Sign.mkArity (ctx2,mk_Prop) + Sign.mkArity (ctx1,prop_sort), Sign.mkArity (ctx2,prop_sort) | Type _ -> (* The type in the interface is inferred and the type in the implementation is not inferred or is inferred but from a |