Préparation du prétypage à la mise en place d'univers algébriques

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

1 files changed, 16 insertions, 2 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index dc8fe35680..86849619d8 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -118,13 +118,27 @@ let new_isevar_sign env sigma typ instance =
 
 (* We don't try to guess in which sort the type should be defined, since
    any type has type Type. May cause some trouble, but not so far... *)
-let dummy_sort = mkType dummy_univ
+(*
+let new_Type () = mkType (new_univ ())
+
+let new_Type_sort () = Type (new_univ ())
+
+let judge_of_new_Type () = fst (Typeops.judge_of_type (new_univ ()))
+*)
+let new_Type () = mkType dummy_univ
+
+let new_Type_sort () = Type dummy_univ
+
+let judge_of_new_Type () = 
+  { uj_val = mkSort (Type dummy_univ);
+    uj_type = mkSort (Type dummy_univ) }
+
 
 (* Declaring any type to be in the sort Type shouldn't be harmful since
    cumulativity now includes Prop and Set in Type. *)
 let new_type_var env sigma =
   let instance = make_evar_instance env in
-  let (sigma',c) = new_isevar_sign env sigma dummy_sort instance in
+  let (sigma',c) = new_isevar_sign env sigma (new_Type ()) instance in
   (sigma', c)
 
 let split_evar_to_arrow sigma c =