aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check_stat.ml18
-rw-r--r--checker/checker.ml14
-rw-r--r--checker/cic.mli7
-rw-r--r--checker/environ.ml25
-rw-r--r--checker/environ.mli4
-rw-r--r--checker/indtypes.ml4
-rw-r--r--checker/reduction.ml7
-rw-r--r--checker/safe_typing.ml22
-rw-r--r--checker/typeops.ml2
-rw-r--r--checker/values.ml6
-rw-r--r--kernel/declarations.mli5
-rw-r--r--kernel/environ.ml17
-rw-r--r--kernel/environ.mli7
-rw-r--r--kernel/fast_typeops.ml6
-rw-r--r--kernel/indtypes.ml2
-rw-r--r--kernel/pre_env.ml6
-rw-r--r--kernel/pre_env.mli3
-rw-r--r--kernel/safe_typing.ml26
-rw-r--r--kernel/safe_typing.mli5
-rw-r--r--kernel/typeops.ml6
-rw-r--r--library/global.ml1
-rw-r--r--library/global.mli1
-rw-r--r--pretyping/nativenorm.ml6
-rw-r--r--toplevel/command.ml3
-rw-r--r--toplevel/coqtop.ml15
-rw-r--r--toplevel/record.ml2
26 files changed, 119 insertions, 101 deletions
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 05a2a1b99..d041f1b7e 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -23,11 +23,17 @@ let print_memory_stat () =
let output_context = ref false
-let pr_engt = function
- Some ImpredicativeSet ->
- str "Theory: Set is impredicative"
- | None ->
- str "Theory: Set is predicative"
+let pr_engagement (impr_set,type_in_type) =
+ begin
+ match impr_set with
+ | ImpredicativeSet -> str "Theory: Set is impredicative"
+ | PredicativeSet -> str "Theory: Set is predicative"
+ end ++
+ begin
+ match type_in_type with
+ | StratifiedType -> str "Theory: Stratified type hierarchy"
+ | TypeInType -> str "Theory: Type is of type Type"
+ end
let cst_filter f csts =
Cmap_env.fold
@@ -54,7 +60,7 @@ let print_context env =
ppnl(hov 0
(fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
str"===============" ++ fnl() ++ fnl() ++
- str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++
+ str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++
str "* " ++ hov 0 (pr_ax csts) ++
fnl())); pp_flush()
end
diff --git a/checker/checker.ml b/checker/checker.ml
index 0f7ed8df5..d5d9b9e3b 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -138,10 +138,11 @@ let init_load_path () =
let set_debug () = Flags.debug := true
-let engagement = ref None
-let set_engagement c = engagement := Some c
-let engage () =
- match !engagement with Some c -> Safe_typing.set_engagement c | None -> ()
+let impredicative_set = ref Cic.PredicativeSet
+let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet
+let type_in_type = ref Cic.StratifiedType
+let set_type_in_type () = type_in_type := Cic.TypeInType
+let engage () = Safe_typing.set_engagement (!impredicative_set,!type_in_type)
let admit_list = ref ([] : section_path list)
@@ -194,6 +195,7 @@ let print_usage_channel co command =
\n -silent disable trace of constants being checked\
\n\
\n -impredicative-set set sort Set impredicative\
+\n -type-in-type collapse type hierarchy\
\n\
\n -h, --help print this list of options\
\n"
@@ -319,7 +321,9 @@ let parse_args argv =
let rec parse = function
| [] -> ()
| "-impredicative-set" :: rem ->
- set_engagement Cic.ImpredicativeSet; parse rem
+ set_impredicative_set (); parse rem
+ | "-type-in-type" :: rem ->
+ set_type_in_type (); parse rem
| "-coqlib" :: s :: rem ->
if not (exists_dir s) then
diff --git a/checker/cic.mli b/checker/cic.mli
index d75af7654..881d3ca79 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -165,7 +165,10 @@ type action
(** Engagements *)
-type engagement = ImpredicativeSet
+type set_predicativity = ImpredicativeSet | PredicativeSet
+type type_hierarchy = TypeInType | StratifiedType
+
+type engagement = set_predicativity * type_hierarchy
(** {6 Representation of constants (Definition/Axiom) } *)
@@ -407,7 +410,7 @@ type compiled_library = {
comp_name : compilation_unit_name;
comp_mod : module_body;
comp_deps : library_deps;
- comp_enga : engagement option;
+ comp_enga : engagement;
comp_natsymbs : nativecode_symb_array
}
diff --git a/checker/environ.ml b/checker/environ.ml
index c0f366000..6dbc44d6b 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -14,7 +14,7 @@ type globals = {
type stratification = {
env_universes : Univ.universes;
- env_engagement : engagement option
+ env_engagement : engagement
}
type env = {
@@ -33,19 +33,28 @@ let empty_env = {
env_rel_context = [];
env_stratification =
{ env_universes = Univ.initial_universes;
- env_engagement = None};
+ env_engagement = (PredicativeSet,StratifiedType)};
env_imports = MPmap.empty }
let engagement env = env.env_stratification.env_engagement
let universes env = env.env_stratification.env_universes
let rel_context env = env.env_rel_context
-let set_engagement c env =
- match env.env_stratification.env_engagement with
- | Some c' -> if c=c' then env else error "Incompatible engagement"
- | None ->
- { env with env_stratification =
- { env.env_stratification with env_engagement = Some c } }
+let set_engagement (impr_set,type_in_type as c) env =
+ let expected_impr_set,expected_type_in_type =
+ env.env_stratification.env_engagement in
+ begin
+ match impr_set,expected_impr_set with
+ | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement"
+ | _ -> ()
+ end;
+ begin
+ match type_in_type,expected_type_in_type with
+ | StratifiedType, TypeInType -> error "Incompatible engagement"
+ | _ -> ()
+ end;
+ { env with env_stratification =
+ { env.env_stratification with env_engagement = c } }
(* Digests *)
diff --git a/checker/environ.mli b/checker/environ.mli
index 22fe7d8f1..f3b2dd839 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -11,7 +11,7 @@ type globals = {
env_modtypes : module_type_body MPmap.t}
type stratification = {
env_universes : Univ.universes;
- env_engagement : engagement option;
+ env_engagement : engagement;
}
type env = {
env_globals : globals;
@@ -22,7 +22,7 @@ type env = {
val empty_env : env
(* Engagement *)
-val engagement : env -> Cic.engagement option
+val engagement : env -> Cic.engagement
val set_engagement : Cic.engagement -> env -> env
(* Digests *)
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 050c33e60..e1a6bc7c1 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -176,7 +176,7 @@ let typecheck_arity env params inds =
(* Allowed eliminations *)
let check_predicativity env s small level =
- match s, engagement env with
+ match s, fst (engagement env) with
Type u, _ ->
(* let u' = fresh_local_univ () in *)
(* let cst = *)
@@ -184,7 +184,7 @@ let check_predicativity env s small level =
(* (universes env) in *)
if not (Univ.check_leq (universes env) level u) then
failwith "impredicative Type inductive type"
- | Prop Pos, Some ImpredicativeSet -> ()
+ | Prop Pos, ImpredicativeSet -> ()
| Prop Pos, _ ->
if not small then failwith "impredicative Set inductive type"
| Prop Null,_ -> ()
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 58f0f894f..8ddeea2a2 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -158,7 +158,7 @@ type conv_pb =
| CONV
| CUMUL
-let sort_cmp univ pb s0 s1 =
+let sort_cmp env univ pb s0 s1 =
match (s0,s1) with
| (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible
| (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible
@@ -167,7 +167,8 @@ let sort_cmp univ pb s0 s1 =
CUMUL -> ()
| _ -> raise NotConvertible)
| (Type u1, Type u2) ->
- if not
+ if snd (engagement env) == StratifiedType
+ && not
(match pb with
| CONV -> Univ.check_eq univ u1 u2
| CUMUL -> Univ.check_leq univ u1 u2)
@@ -261,7 +262,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(match a1, a2 with
| (Sort s1, Sort s2) ->
assert (is_empty_stack v1 && is_empty_stack v2);
- sort_cmp univ cv_pb s1 s2
+ sort_cmp (infos_env infos) univ cv_pb s1 s2
| (Meta n, Meta m) ->
if n=m
then convert_stacks univ infos lft1 lft2 v1 v2
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 810d6e0b6..dd9482313 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -32,13 +32,21 @@ let full_add_module dp mb univs digest =
let env = Modops.add_module mb env in
genv := add_digest env dp digest
-(* Check that the engagement expected by a library matches the initial one *)
-let check_engagement env c =
- match engagement env, c with
- | Some ImpredicativeSet, Some ImpredicativeSet -> ()
- | _, None -> ()
- | _, Some ImpredicativeSet ->
- error "Needs option -impredicative-set"
+(* Check that the engagement expected by a library extends the initial one *)
+let check_engagement env (expected_impredicative_set,expected_type_in_type) =
+ let impredicative_set,type_in_type = Environ.engagement env in
+ begin
+ match impredicative_set, expected_impredicative_set with
+ | PredicativeSet, ImpredicativeSet ->
+ Errors.error "Needs option -impredicative-set."
+ | _ -> ()
+ end;
+ begin
+ match type_in_type, expected_type_in_type with
+ | StratifiedType, TypeInType ->
+ Errors.error "Needs option -type-in-type."
+ | _ -> ()
+ end
(* Libraries = Compiled modules *)
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 9bc4b269b..21819992a 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -128,7 +128,7 @@ let sort_of_product env domsort rangsort =
| (Prop _, Prop Pos) -> rangsort
(* Product rule (Type,Set,?) *)
| (Type u1, Prop Pos) ->
- if engagement env = Some ImpredicativeSet then
+ if fst (engagement env) = ImpredicativeSet then
(* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
rangsort
else
diff --git a/checker/values.ml b/checker/values.ml
index 46b66adc4..e82ba1032 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -193,7 +193,9 @@ let v_lazy_constr =
(** kernel/declarations *)
-let v_engagement = v_enum "eng" 1
+let v_impredicative_set = v_enum "impr-set" 2
+let v_type_in_type = v_enum "type-in-type" 2
+let v_engagement = v_tuple "eng" [|v_impredicative_set; v_type_in_type|]
let v_pol_arity =
v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
@@ -315,7 +317,7 @@ and v_modtype =
let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |])
let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|])
let v_compiled_lib =
- v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|]
+ v_tuple "compiled" [|v_dp;v_module;v_deps;v_engagement;Any|]
(** Library objects *)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index c1c19a757..561c66b42 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -14,7 +14,10 @@ open Context
declarations. This includes global constants/axioms, mutual
inductive definitions, modules and module types *)
-type engagement = ImpredicativeSet
+type set_predicativity = ImpredicativeSet | PredicativeSet
+type type_hierarchy = TypeInType | StratifiedType
+
+type engagement = set_predicativity * type_hierarchy
(** {6 Representation of constants (Definition/Axiom) } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a79abbb7e..30b28177c 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -46,11 +46,14 @@ let empty_env = empty_env
let engagement env = env.env_stratification.env_engagement
-let type_in_type env = env.env_stratification.env_type_in_type
-
let is_impredicative_set env =
- match engagement env with
- | Some ImpredicativeSet -> true
+ match fst (engagement env) with
+ | ImpredicativeSet -> true
+ | _ -> false
+
+let type_in_type env =
+ match snd (engagement env) with
+ | TypeInType -> true
| _ -> false
let universes env = env.env_stratification.env_universes
@@ -191,11 +194,7 @@ let check_constraints c env =
let set_engagement c env = (* Unsafe *)
{ env with env_stratification =
- { env.env_stratification with env_engagement = Some c } }
-
-let set_type_in_type env =
- { env with env_stratification =
- { env.env_stratification with env_type_in_type = true } }
+ { env.env_stratification with env_engagement = c } }
let push_constraints_to_env (_,univs) env =
add_constraints univs env
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ede356e69..4ad0327fc 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -50,10 +50,9 @@ val opaque_tables : env -> Opaqueproof.opaquetab
val set_opaque_tables : env -> Opaqueproof.opaquetab -> env
-val engagement : env -> engagement option
+val engagement : env -> engagement
val is_impredicative_set : env -> bool
-
-val type_in_type : env -> bool
+val type_in_type : env -> bool
(** is the local context empty *)
val empty_context : env -> bool
@@ -215,8 +214,6 @@ val push_constraints_to_env : 'a Univ.constrained -> env -> env
val set_engagement : engagement -> env -> env
-val set_type_in_type : env -> env
-
(** {6 Sets of referred section variables }
[global_vars_set env c] returns the list of [id]'s occurring either
directly as [Var id] in [c] or indirectly as a section variable
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 86fb1b64c..d22abff10 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -182,14 +182,12 @@ let sort_of_product env domsort rangsort =
| (Prop _, Prop Pos) -> rangsort
(* Product rule (Type,Set,?) *)
| (Type u1, Prop Pos) ->
- begin match engagement env with
- | Some ImpredicativeSet ->
+ if is_impredicative_set env then
(* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
rangsort
- | _ ->
+ else
(* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
Type (Universe.sup Universe.type0 u1)
- end
(* Product rule (Prop,Type_i,Type_i) *)
| (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2)
(* Product rule (Prop,Type_i,Type_i) *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 31c0e83c8..9c79009db 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -173,7 +173,7 @@ let cumulate_arity_large_levels env sign =
sign (Universe.type0m,env))
let is_impredicative env u =
- is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet)
+ is_type0m_univ u || (is_type0_univ u && is_impredicative_set env)
(* Returns the list [x_1, ..., x_n] of levels contributing to template
polymorphism. The elements x_k is None if the k-th parameter (starting
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 557ed3d7d..5f3f559a2 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -46,8 +46,7 @@ type globals = {
type stratification = {
env_universes : universes;
- env_engagement : engagement option;
- env_type_in_type : bool
+ env_engagement : engagement
}
type val_kind =
@@ -95,8 +94,7 @@ let empty_env = {
env_nb_rel = 0;
env_stratification = {
env_universes = initial_universes;
- env_engagement = None;
- env_type_in_type = false};
+ env_engagement = (PredicativeSet,StratifiedType) };
env_conv_oracle = Conv_oracle.empty;
retroknowledge = Retroknowledge.initial_retroknowledge;
indirect_pterms = Opaqueproof.empty_opaquetab }
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 03ac41b45..0ce0bed23 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -33,8 +33,7 @@ type globals = {
type stratification = {
env_universes : universes;
- env_engagement : engagement option;
- env_type_in_type : bool
+ env_engagement : engagement
}
type lazy_val
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d8473183a..907ad2a1d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -184,16 +184,20 @@ let set_engagement c senv =
(** Check that the engagement [c] expected by a library matches
the current (initial) one *)
-let check_engagement env c =
- match Environ.engagement env, c with
- | None, Some ImpredicativeSet ->
- Errors.error "Needs option -impredicative-set."
- | _ -> ()
-
-let set_type_in_type senv =
- { senv with
- env = Environ.set_type_in_type senv.env;
- type_in_type = true }
+let check_engagement env (expected_impredicative_set,expected_type_in_type) =
+ let impredicative_set,type_in_type = Environ.engagement env in
+ begin
+ match impredicative_set, expected_impredicative_set with
+ | PredicativeSet, ImpredicativeSet ->
+ Errors.error "Needs option -impredicative-set."
+ | _ -> ()
+ end;
+ begin
+ match type_in_type, expected_type_in_type with
+ | StratifiedType, TypeInType ->
+ Errors.error "Needs option -type-in-type."
+ | _ -> ()
+ end
(** {6 Stm machinery } *)
@@ -734,7 +738,7 @@ type compiled_library = {
comp_name : DirPath.t;
comp_mod : module_body;
comp_deps : library_info array;
- comp_enga : engagement option;
+ comp_enga : engagement;
comp_natsymbs : Nativecode.symbols
}
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 1e9cdbda0..2b4324b96 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -99,12 +99,9 @@ val add_constraints :
(* (\** Generator of universes *\) *)
(* val next_universe : int safe_transformer *)
-(** Setting the strongly constructive or classical logical engagement *)
+(** Setting the type theory flavor *)
val set_engagement : Declarations.engagement -> safe_transformer0
-(** Collapsing the type hierarchy *)
-val set_type_in_type : safe_transformer0
-
(** {6 Interactive module functions } *)
val start_module : Label.t -> module_path safe_transformer
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 48dbacf1a..fe82d85d5 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -252,14 +252,12 @@ let sort_of_product env domsort rangsort =
| (Prop _, Prop Pos) -> rangsort
(* Product rule (Type,Set,?) *)
| (Type u1, Prop Pos) ->
- begin match engagement env with
- | Some ImpredicativeSet ->
+ if is_impredicative_set env then
(* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
rangsort
- | _ ->
+ else
(* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
Type (Universe.sup Universe.type0 u1)
- end
(* Product rule (Prop,Type_i,Type_i) *)
| (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2)
(* Product rule (Prop,Type_i,Type_i) *)
diff --git a/library/global.ml b/library/global.ml
index 49fa2ef28..0419799b6 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -84,7 +84,6 @@ let push_context_set c = globalize0 (Safe_typing.push_context_set c)
let push_context c = globalize0 (Safe_typing.push_context c)
let set_engagement c = globalize0 (Safe_typing.set_engagement c)
-let set_type_in_type () = globalize0 (Safe_typing.set_type_in_type)
let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d)
let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie)
let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
diff --git a/library/global.mli b/library/global.mli
index 75a1ebee9..363bb5789 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -27,7 +27,6 @@ val named_context : unit -> Context.named_context
(** Changing the (im)predicativity of the system *)
val set_engagement : Declarations.engagement -> unit
-val set_type_in_type : unit -> unit
(** Variables, Local definitions, constants, inductive types *)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index b4b6b8aab..2432b8d29 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -150,14 +150,12 @@ let sort_of_product env domsort rangsort =
| (Prop _, Prop Pos) -> rangsort
(* Product rule (Type,Set,?) *)
| (Type u1, Prop Pos) ->
- begin match engagement env with
- | Some ImpredicativeSet ->
+ if is_impredicative_set env then
(* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
rangsort
- | _ ->
+ else
(* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
Type (sup u1 type0_univ)
- end
(* Product rule (Prop,Type_i,Type_i) *)
| (Prop Pos, Type u2) -> Type (sup type0_univ u2)
(* Product rule (Prop,Type_i,Type_i) *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 77339aef4..04238da2b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -360,8 +360,7 @@ let make_conclusion_flexible evdref ty poly =
else ()
let is_impredicative env u =
- u = Prop Null ||
- (engagement env = Some Declarations.ImpredicativeSet && u = Prop Pos)
+ u = Prop Null || (is_impredicative_set env && u = Prop Pos)
let interp_ind_arity env evdref ind =
let c = intern_gen IsType env ind.ind_arity in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 5b330cd25..5540dc0ff 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -112,14 +112,12 @@ let print_memory_stat () =
let _ = at_exit print_memory_stat
-let engagement = ref None
-let set_engagement c = engagement := Some c
+let impredicative_set = ref Declarations.PredicativeSet
+let set_impredicative_set c = impredicative_set := Declarations.ImpredicativeSet
+let type_in_type = ref Declarations.StratifiedType
+let set_type_in_type () = type_in_type := Declarations.TypeInType
let engage () =
- match !engagement with Some c -> Global.set_engagement c | None -> ()
-
-let type_in_type = ref false
-let set_type_in_type () = type_in_type := true
-let set_hierarchy () = if !type_in_type then Global.set_type_in_type ()
+ Global.set_engagement (!impredicative_set,!type_in_type)
let set_batch_mode () = batch_mode := true
@@ -521,7 +519,7 @@ let parse_args arglist =
|"-filteropts" -> filter_opts := true
|"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
|"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true
- |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet
+ |"-impredicative-set" -> set_impredicative_set ()
|"-indices-matter" -> Indtypes.enforce_indices_matter ()
|"-just-parsing" -> Vernac.just_parsing := true
|"-m"|"--memory" -> memory_stat := true
@@ -605,7 +603,6 @@ let init arglist =
Mltop.init_known_plugins ();
set_vm_opt ();
engage ();
- set_hierarchy ();
(* Be careful to set these variables after the inputstate *)
Syntax_def.set_verbose_compat_notations !verb_compat_ntn;
Syntax_def.set_compat_notations (not !no_compat_ntn);
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 737b7fb59..15ad18d9c 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -135,7 +135,7 @@ let typecheck_params_and_fields def id t ps nots fs =
let ctx, aritysort = Reduction.dest_arity env0 arity in
assert(List.is_empty ctx); (* Ensured by above analysis *)
if Sorts.is_prop aritysort ||
- (Sorts.is_set aritysort && engagement env0 = Some ImpredicativeSet) then
+ (Sorts.is_set aritysort && is_impredicative_set env0) then
evars
else Evd.set_leq_sort env_ar evars (Type univ) aritysort
in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 03:07:09 +0000