diff options
Diffstat (limited to 'checker/values.ml')
| -rw-r--r-- | checker/values.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/values.ml b/checker/values.ml index 4f28d6e44..88cdb644d 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -15,7 +15,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 42fb0781dc5f7f2cbe3ca127f8249264 checker/cic.mli +MD5 c395aa2dbfc18794b3b7192f3dc5b2e5 checker/cic.mli *) @@ -122,7 +122,7 @@ let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|] (** kernel/term *) -let v_sort = v_sum "sort" 0 [|[|v_enum "cnt" 2|];[|v_univ|]|] +let v_sort = v_sum "sort" 2 (*Prop, Set*) [|[|v_univ(*Type*)|]|] let v_sortfam = v_enum "sorts_family" 3 let v_puniverses v = v_tuple "punivs" [|v;v_instance|] |