From 382e4f6bb67bec64ea4a0ead5e9de232858a891e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 9 Sep 2001 15:39:40 +0000
Subject: Passage aux univers algébriques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1940 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarutil.ml | 5 ++---
 pretyping/retyping.ml | 4 ++--
 2 files changed, 4 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 86849619d8..f23a9c7a12 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -118,13 +118,12 @@ 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 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
@@ -132,7 +131,7 @@ 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. *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index a2b98a6d82..f75537e574 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -85,11 +85,11 @@ let typeur sigma metamap =
     match kind_of_term t with
     | IsCast (c,s) when isSort s -> destSort s
     | IsSort (Prop c) -> type_0
-    | IsSort (Type u) -> Type Univ.dummy_univ
+    | IsSort (Type u) -> Type (fst (Univ.super u))
     | IsProd (name,t,c2) ->
         (match (sort_of (push_rel_assum (name,t) env) c2) with
 	  | Prop _ as s -> s
-	  | Type u2 -> Type Univ.dummy_univ)
+	  | Type u2 as s -> s (*Type Univ.dummy_univ*))
     | IsApp(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
     | IsLambda _ | IsFix _ | IsMutConstruct _ ->
         anomaly "sort_of: Not a type (1)"
-- 
cgit v1.2.3