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

4 files changed, 26 insertions, 12 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 038f70c2c2..864632ebb0 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -60,7 +60,7 @@ let error_needs_inversion k env x t =
 (* A) Typing old cases                                               *)
 (* This was previously in Indrec but creates existential holes       *)
 
-let mkExistential isevars env = new_isevar isevars env dummy_sort CCI
+let mkExistential isevars env = new_isevar isevars env (new_Type ()) CCI
 
 let norec_branch_scheme env isevars cstr =
   let rec crec env = function
@@ -958,9 +958,9 @@ let find_predicate env isevars p typs cstrs current (IndType (indf,realargs)) =
       | None -> infer_predicate env isevars typs cstrs indf in
   let typ = whd_beta (applist (pred, realargs)) in
   if dep then
-    (pred, whd_beta (applist (typ, [current])), Type Univ.dummy_univ)
+    (pred, whd_beta (applist (typ, [current])), new_Type ())
   else
-    (pred, typ, Type Univ.dummy_univ)
+    (pred, typ, new_Type ())
 
 (************************************************************************)
 (* Sorting equation by constructor *)
@@ -1328,7 +1328,7 @@ let build_expected_arity env isevars isdep tomatchl =
     | _,NotInd _ -> None
   in
   let rec buildrec n env = function
-    | [] -> dummy_sort
+    | [] -> new_Type ()
     | tm::ltm ->
 	match cook n tm with
 	  | None -> buildrec n env ltm
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 =
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 0295b7dfec..2d6681f815 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -64,7 +64,9 @@ val solve_simple_eqn :
 
 (* Value/Type constraints *)
 
-val dummy_sort : constr
+val new_Type_sort : unit -> sorts
+val new_Type : unit -> constr
+val judge_of_new_Type : unit -> unsafe_judgment
 
 type type_constraint = constr option
 type val_constraint = constr option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index bb01b16197..5f6a418ebf 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -194,9 +194,7 @@ let pretype_ref _ isevars env lvar ref =
 *)
 let pretype_sort = function
   | RProp c -> judge_of_prop_contents c
-  | RType _ ->
-      { uj_val = dummy_sort;
-	uj_type = dummy_sort }
+  | RType _ -> judge_of_new_Type ()
 
 (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
 (* in environment [env], with existential variables [(evars_of isevars)] and *)
@@ -443,8 +441,8 @@ and pretype_type valcon env isevars lvar lmeta = function
 	     { utj_val = v;
 	       utj_type = Retyping.get_sort_of env (evars_of isevars) v }
 	 | None ->
-	     { utj_val = new_isevar isevars env dummy_sort CCI;
-	       utj_type = Type Univ.dummy_univ })
+	     let s = new_Type_sort () in
+	     { utj_val = new_isevar isevars env (mkSort s) CCI; utj_type = s})
   | c ->
       let j = pretype empty_tycon env isevars lvar lmeta c in
       let tj = inh_coerce_to_sort env isevars j in