Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles des sortes (InProp, InSet, InType)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 2 deletions

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