From f83572bc45b9ab6b72688eb22d125896541ccf16 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 19 Sep 2001 16:55:41 +0000 Subject: Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles des sortes (InProp, InSet, InType) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/term.ml | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) (limited to 'kernel/term.ml') diff --git a/kernel/term.ml b/kernel/term.ml index 1637fcafb..8b276c068 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -45,6 +45,18 @@ let print_sort = function (* | Type _ -> [< 'sTR "Type" >] *) | Type u -> [< 'sTR "Type("; pr_uni u; 'sTR ")" >] +type sorts_family = InProp | InSet | InType + +let new_sort_in_family = function + | InProp -> mk_Prop + | InSet -> mk_Set + | InType -> Type (Univ.new_univ ()) + +let family_of_sort = function + | Prop Null -> InProp + | Prop Pos -> InSet + | Type _ -> InType + (********************************************************************) (* type of global reference *) @@ -1057,8 +1069,8 @@ let mkProp = mkSort mk_Prop let mkSet = mkSort mk_Set let mkType u = mkSort (Type u) -let prop = Prop Null -and spec = Prop Pos +let prop = mk_Prop +and spec = mk_Set and types = Type implicit_univ (* For eliminations *) and type_0 = Type prop_univ -- cgit v1.2.3