diff options
| author | herbelin | 2001-09-09 15:39:40 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-09 15:39:40 +0000 |
| commit | 382e4f6bb67bec64ea4a0ead5e9de232858a891e (patch) | |
| tree | 99f79d0e8fa93366acb90788443aad2b0bc25043 /pretyping | |
| parent | 106d1c36ced53924f9dd3965e40536b2d1d3fb31 (diff) | |
Passage aux univers algébriques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1940 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 5 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 4 |
2 files changed, 4 insertions, 5 deletions
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)" |