aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/declarations.mli3
-rw-r--r--kernel/environ.ml11
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/fast_typeops.ml69
-rw-r--r--kernel/fast_typeops.mli6
-rw-r--r--kernel/inductive.ml6
-rw-r--r--kernel/inductive.mli4
-rw-r--r--kernel/pre_env.ml5
-rw-r--r--kernel/pre_env.mli1
-rw-r--r--kernel/safe_typing.ml33
-rw-r--r--kernel/safe_typing.mli5
-rw-r--r--kernel/term_typing.ml43
-rw-r--r--kernel/term_typing.mli12
-rw-r--r--kernel/typeops.ml4
-rw-r--r--library/declare.ml22
-rw-r--r--library/declare.mli2
-rw-r--r--library/global.ml5
-rw-r--r--library/global.mli5
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--pretyping/inductiveops.ml4
-rw-r--r--pretyping/pretyping.ml15
-rw-r--r--pretyping/pretyping.mli2
-rw-r--r--pretyping/typing.ml4
-rw-r--r--printing/printer.ml2
-rw-r--r--stm/lemmas.ml2
-rw-r--r--toplevel/command.ml47
-rw-r--r--toplevel/command.mli11
-rw-r--r--toplevel/coqtop.ml7
-rw-r--r--toplevel/obligations.ml2
-rw-r--r--toplevel/vernacentries.ml14
30 files changed, 175 insertions, 175 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 639cd061b..ef4d398c1 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -14,9 +14,8 @@ open Term
inductive definitions, modules and module types *)
type set_predicativity = ImpredicativeSet | PredicativeSet
-type type_hierarchy = TypeInType | StratifiedType
-type engagement = set_predicativity * type_hierarchy
+type engagement = set_predicativity
(** {6 Representation of constants (Definition/Axiom) } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 032e71359..65aaa3f7b 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -45,16 +45,14 @@ let empty_named_context_val = empty_named_context_val
let empty_env = empty_env
let engagement env = env.env_stratification.env_engagement
+let typing_flags env = env.env_typing_flags
let is_impredicative_set env =
- match fst (engagement env) with
+ match engagement env with
| ImpredicativeSet -> true
| _ -> false
-let type_in_type env =
- match snd (engagement env) with
- | TypeInType -> true
- | _ -> false
+let type_in_type env = not (typing_flags env).check_universes
let universes env = env.env_stratification.env_universes
let named_context env = env.env_named_context
@@ -211,6 +209,9 @@ let set_engagement c env = (* Unsafe *)
{ env with env_stratification =
{ env.env_stratification with env_engagement = c } }
+let set_typing_flags c env = (* Unsafe *)
+ { env with env_typing_flags = c }
+
(* Global constants *)
let lookup_constant = lookup_constant
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 7ce1cea27..0edcb34de 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -50,6 +50,7 @@ val set_opaque_tables : env -> Opaqueproof.opaquetab -> env
val engagement : env -> engagement
+val typing_flags : env -> typing_flags
val is_impredicative_set : env -> bool
val type_in_type : env -> bool
@@ -214,6 +215,7 @@ val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
val push_constraints_to_env : 'a Univ.constrained -> env -> env
val set_engagement : engagement -> env -> env
+val set_typing_flags : typing_flags -> env -> env
(** {6 Sets of referred section variables }
[global_vars_set env c] returns the list of [id]'s occurring either
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 35c162cf3..c2c8ee242 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -327,7 +327,7 @@ let type_fixpoint env lna lar vdef vdeft =
(* ATTENTION : faudra faire le typage du contexte des Const,
Ind et Constructsi un jour cela devient des constructions
arbitraires et non plus des variables *)
-let rec execute ~flags env cstr =
+let rec execute env cstr =
let open Context.Rel.Declaration in
match kind_of_term cstr with
(* Atomic terms *)
@@ -347,12 +347,12 @@ let rec execute ~flags env cstr =
judge_of_constant env c
| Proj (p, c) ->
- let ct = execute ~flags env c in
+ let ct = execute env c in
judge_of_projection env p c ct
(* Lambda calculus operators *)
| App (f,args) ->
- let argst = execute_array ~flags env args in
+ let argst = execute_array env args in
let ft =
match kind_of_term f with
| Ind ind when Environ.template_polymorphic_pind ind env ->
@@ -365,7 +365,7 @@ let rec execute ~flags env cstr =
judge_of_constant_knowing_parameters env cst args
| _ ->
(* Full or no sort-polymorphism *)
- execute ~flags env f
+ execute env f
in
judge_of_apply env f ft args argst
@@ -373,25 +373,25 @@ let rec execute ~flags env cstr =
| Lambda (name,c1,c2) ->
let _ = execute_is_type env c1 in
let env1 = push_rel (LocalAssum (name,c1)) env in
- let c2t = execute ~flags env1 c2 in
+ let c2t = execute env1 c2 in
judge_of_abstraction env name c1 c2t
| Prod (name,c1,c2) ->
- let vars = execute_is_type ~flags env c1 in
+ let vars = execute_is_type env c1 in
let env1 = push_rel (LocalAssum (name,c1)) env in
- let vars' = execute_is_type ~flags env1 c2 in
+ let vars' = execute_is_type env1 c2 in
judge_of_product env name vars vars'
| LetIn (name,c1,c2,c3) ->
- let c1t = execute ~flags env c1 in
+ let c1t = execute env c1 in
let _c2s = execute_is_type env c2 in
let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in
let env1 = push_rel (LocalDef (name,c1,c2)) env in
- let c3t = execute ~flags env1 c3 in
+ let c3t = execute env1 c3 in
subst1 c1 c3t
| Cast (c,k,t) ->
- let ct = execute ~flags env c in
+ let ct = execute env c in
let _ts = execute_type env t in
let _ = judge_of_cast env c ct k t in
t
@@ -404,20 +404,20 @@ let rec execute ~flags env cstr =
judge_of_constructor env c
| Case (ci,p,c,lf) ->
- let ct = execute ~flags env c in
- let pt = execute ~flags env p in
- let lft = execute_array ~flags env lf in
+ let ct = execute env c in
+ let pt = execute env p in
+ let lft = execute_array env lf in
judge_of_case env ci p pt c ct lf lft
| Fix ((vn,i as vni),recdef) ->
- let (fix_ty,recdef') = execute_recdef ~flags env recdef i in
+ let (fix_ty,recdef') = execute_recdef env recdef i in
let fix = (vni,recdef') in
- check_fix env ~flags fix; fix_ty
+ check_fix env fix; fix_ty
| CoFix (i,recdef) ->
- let (fix_ty,recdef') = execute_recdef ~flags env recdef i in
+ let (fix_ty,recdef') = execute_recdef env recdef i in
let cofix = (i,recdef') in
- check_cofix env ~flags cofix; fix_ty
+ check_cofix env cofix; fix_ty
(* Partial proofs: unsupported by the kernel *)
| Meta _ ->
@@ -426,41 +426,38 @@ let rec execute ~flags env cstr =
| Evar _ ->
anomaly (Pp.str "the kernel does not support existential variables")
-and execute_is_type ~flags env constr =
- let t = execute ~flags env constr in
+and execute_is_type env constr =
+ let t = execute env constr in
check_type env constr t
-and execute_type ~flags env constr =
- let t = execute ~flags env constr in
+and execute_type env constr =
+ let t = execute env constr in
type_judgment env constr t
-and execute_recdef ~flags env (names,lar,vdef) i =
- let lart = execute_array ~flags env lar in
+and execute_recdef env (names,lar,vdef) i =
+ let lart = execute_array env lar in
let lara = Array.map2 (assumption_of_judgment env) lar lart in
let env1 = push_rec_types (names,lara,vdef) env in
- let vdeft = execute_array ~flags env1 vdef in
+ let vdeft = execute_array env1 vdef in
let () = type_fixpoint env1 names lara vdef vdeft in
(lara.(i),(names,lara,vdef))
-and execute_array ~flags env = Array.map (execute ~flags env)
+and execute_array env = Array.map (execute env)
(* Derived functions *)
-let infer ~flags env constr =
- let t = execute ~flags env constr in
+let infer env constr =
+ let t = execute env constr in
make_judge constr t
let infer =
if Flags.profile then
let infer_key = Profile.declare_profile "Fast_infer" in
- Profile.profile3 infer_key (fun a b c -> infer ~flags:a b c)
- else (fun a b c -> infer ~flags:a b c)
+ Profile.profile2 infer_key (fun b c -> infer b c)
+ else (fun b c -> infer b c)
-(* Restores the labels of [infer] lost to profiling. *)
-let infer ~flags env t = infer flags env t
+let infer_type env constr =
+ execute_type env constr
-let infer_type ~flags env constr =
- execute_type ~flags env constr
-
-let infer_v ~flags env cv =
- let jv = execute_array ~flags env cv in
+let infer_v env cv =
+ let jv = execute_array env cv in
make_judgev cv jv
diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli
index 45a603038..41cff607e 100644
--- a/kernel/fast_typeops.mli
+++ b/kernel/fast_typeops.mli
@@ -19,6 +19,6 @@ open Declarations
*)
-val infer : flags:typing_flags -> env -> constr -> unsafe_judgment
-val infer_v : flags:typing_flags -> env -> constr array -> unsafe_judgment array
-val infer_type : flags:typing_flags -> env -> types -> unsafe_type_judgment
+val infer : env -> constr -> unsafe_judgment
+val infer_v : env -> constr array -> unsafe_judgment array
+val infer_type : env -> types -> unsafe_type_judgment
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 24bdaa5c4..8e26370ec 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1067,7 +1067,8 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
(Array.map fst rv, Array.map snd rv)
-let check_fix env ~flags ((nvect,_),(names,_,bodies as recdef) as fix) =
+let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
+ let flags = Environ.typing_flags env in
if flags.check_guarded then
let (minds, rdef) = inductive_of_mutfix env fix in
let get_tree (kn,i) =
@@ -1195,7 +1196,8 @@ let check_one_cofix env nbfix def deftype =
(* The function which checks that the whole block of definitions
satisfies the guarded condition *)
-let check_cofix env ~flags (bodynum,(names,types,bodies as recdef)) =
+let check_cofix env (bodynum,(names,types,bodies as recdef)) =
+ let flags = Environ.typing_flags env in
if flags.check_guarded then
let nbfix = Array.length bodies in
for i = 0 to nbfix-1 do
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 25a557472..521ee3c7b 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -97,8 +97,8 @@ val check_case_info : env -> pinductive -> case_info -> unit
(** When [chk] is false, the guard condition is not actually
checked. *)
-val check_fix : env -> flags:typing_flags -> fixpoint -> unit
-val check_cofix : env -> flags:typing_flags -> cofixpoint -> unit
+val check_fix : env -> fixpoint -> unit
+val check_cofix : env -> cofixpoint -> unit
(** {6 Support for sort-polymorphic inductive types } *)
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index c30789641..5afefeebd 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -71,6 +71,7 @@ type env = {
env_rel_val : lazy_val list;
env_nb_rel : int;
env_stratification : stratification;
+ env_typing_flags : typing_flags;
env_conv_oracle : Conv_oracle.oracle;
retroknowledge : Retroknowledge.retroknowledge;
indirect_pterms : Opaqueproof.opaquetab;
@@ -93,7 +94,8 @@ let empty_env = {
env_nb_rel = 0;
env_stratification = {
env_universes = UGraph.initial_universes;
- env_engagement = (PredicativeSet,StratifiedType) };
+ env_engagement = PredicativeSet };
+ env_typing_flags = Declareops.safe_flags;
env_conv_oracle = Conv_oracle.empty;
retroknowledge = Retroknowledge.initial_retroknowledge;
indirect_pterms = Opaqueproof.empty_opaquetab }
@@ -138,6 +140,7 @@ let push_named d env =
env_rel_val = env.env_rel_val;
env_nb_rel = env.env_nb_rel;
env_stratification = env.env_stratification;
+ env_typing_flags = env.env_typing_flags;
env_conv_oracle = env.env_conv_oracle;
retroknowledge = env.retroknowledge;
indirect_pterms = env.indirect_pterms;
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 353c46112..e551d22c8 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -50,6 +50,7 @@ type env = {
env_rel_val : lazy_val list;
env_nb_rel : int;
env_stratification : stratification;
+ env_typing_flags : typing_flags;
env_conv_oracle : Conv_oracle.oracle;
retroknowledge : Retroknowledge.retroknowledge;
indirect_pterms : Opaqueproof.opaquetab;
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 72d6ee518..fc6155930 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -180,21 +180,18 @@ let set_engagement c senv =
env = Environ.set_engagement c senv.env;
engagement = Some c }
+let set_typing_flags c senv =
+ { senv with env = Environ.set_typing_flags c senv.env }
+
(** Check that the engagement [c] expected by a library matches
the current (initial) one *)
-let check_engagement env (expected_impredicative_set,expected_type_in_type) =
- let impredicative_set,type_in_type = Environ.engagement env in
+let check_engagement env expected_impredicative_set =
+ let impredicative_set = 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 } *)
@@ -373,8 +370,8 @@ let safe_push_named d env =
Environ.push_named d env
-let push_named_def ~flags (id,de) senv =
- let c,typ,univs = Term_typing.translate_local_def ~flags senv.revstruct senv.env id de in
+let push_named_def (id,de) senv =
+ let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in
let poly = de.Entries.const_entry_polymorphic in
let univs = Univ.ContextSet.of_context univs in
let c, univs = match c with
@@ -388,9 +385,9 @@ let push_named_def ~flags (id,de) senv =
let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in
univs, {senv' with env=env''}
-let push_named_assum ~flags ((id,t,poly),ctx) senv =
+let push_named_assum ((id,t,poly),ctx) senv =
let senv' = push_context_set poly ctx senv in
- let t = Term_typing.translate_local_assum ~flags senv'.env t in
+ let t = Term_typing.translate_local_assum senv'.env t in
let env'' = safe_push_named (LocalAssum (id,t)) senv'.env in
{senv' with env=env''}
@@ -479,7 +476,7 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver }
(** Insertion of constants and parameters in environment *)
type global_declaration =
- | ConstantEntry of bool * private_constants Entries.constant_entry * Declarations.typing_flags
+ | ConstantEntry of bool * private_constants Entries.constant_entry
| GlobalRecipe of Cooking.recipe
type exported_private_constant =
@@ -512,10 +509,10 @@ let add_constant dir l decl senv =
let no_section = DirPath.is_empty dir in
let seff_to_export, decl =
match decl with
- | ConstantEntry (true, ce, flags) ->
+ | ConstantEntry (true, ce) ->
let exports, ce =
- Term_typing.export_side_effects ~flags senv.revstruct senv.env ce in
- exports, ConstantEntry (false, ce, flags)
+ Term_typing.export_side_effects senv.revstruct senv.env ce in
+ exports, ConstantEntry (false, ce)
| _ -> [], decl
in
let senv =
@@ -524,8 +521,8 @@ let add_constant dir l decl senv =
let senv =
let cb =
match decl with
- | ConstantEntry (export_seff,ce,flags) ->
- Term_typing.translate_constant ~flags senv.revstruct senv.env kn ce
+ | ConstantEntry (export_seff,ce) ->
+ Term_typing.translate_constant senv.revstruct senv.env kn ce
| GlobalRecipe r ->
let cb = Term_typing.translate_recipe senv.env kn r in
if no_section then Declareops.hcons_const_body cb else cb in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index b614a368c..15ebc7d88 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -77,21 +77,19 @@ val is_joined_environment : safe_environment -> bool
(** Insertion of local declarations (Local or Variables) *)
val push_named_assum :
- flags:Declarations.typing_flags ->
(Id.t * Term.types * bool (* polymorphic *))
Univ.in_universe_context_set -> safe_transformer0
(** Returns the full universe context necessary to typecheck the definition
(futures are forced) *)
val push_named_def :
- flags:Declarations.typing_flags ->
Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer
(** Insertion of global axioms or definitions *)
type global_declaration =
(* bool: export private constants *)
- | ConstantEntry of bool * private_constants Entries.constant_entry * Declarations.typing_flags
+ | ConstantEntry of bool * private_constants Entries.constant_entry
| GlobalRecipe of Cooking.recipe
type exported_private_constant =
@@ -134,6 +132,7 @@ val add_constraints :
(** Setting the type theory flavor *)
val set_engagement : Declarations.engagement -> safe_transformer0
+val set_typing_flags : Declarations.typing_flags -> safe_transformer0
(** {6 Interactive module functions } *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a7c6ef057..be84cae6d 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -22,18 +22,18 @@ open Entries
open Typeops
open Fast_typeops
-let constrain_type ~flags env j poly subst = function
+let constrain_type env j poly subst = function
| `None ->
if not poly then (* Old-style polymorphism *)
make_polymorphic_if_constant_for_ind env j
else RegularArity (Vars.subst_univs_level_constr subst j.uj_type)
| `Some t ->
- let tj = infer_type ~flags env t in
+ let tj = infer_type env t in
let _ = judge_of_cast env j DEFAULTcast tj in
assert (eq_constr t tj.utj_val);
RegularArity (Vars.subst_univs_level_constr subst t)
| `SomeWJ (t, tj) ->
- let tj = infer_type ~flags env t in
+ let tj = infer_type env t in
let _ = judge_of_cast env j DEFAULTcast tj in
assert (eq_constr t tj.utj_val);
RegularArity (Vars.subst_univs_level_constr subst t)
@@ -171,11 +171,11 @@ let feedback_completion_typecheck =
Option.iter (fun state_id ->
feedback ~id:(State state_id) Feedback.Complete)
-let infer_declaration ~flags ~trust env kn dcl =
+let infer_declaration ~trust env kn dcl =
match dcl with
| ParameterEntry (ctx,poly,(t,uctx),nl) ->
let env = push_context ~strict:(not poly) uctx env in
- let j = infer ~flags env t in
+ let j = infer env t in
let abstract = poly && not (Option.is_empty kn) in
let usubst, univs = Univ.abstract_universes abstract uctx in
let c = Typeops.assumption_of_judgment env j in
@@ -196,7 +196,7 @@ let infer_declaration ~flags ~trust env kn dcl =
let env' = push_context_set uctx env in
let j =
let body,env',ectx = skip_trusted_seff valid_signatures body env' in
- let j = infer ~flags env' body in
+ let j = infer env' body in
unzip ectx j in
let j = hcons_j j in
let subst = Univ.LMap.empty in
@@ -220,8 +220,8 @@ let infer_declaration ~flags ~trust env kn dcl =
let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
let usubst, univs =
Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in
- let j = infer ~flags env body in
- let typ = constrain_type ~flags env j c.const_entry_polymorphic usubst (map_option_typ typ) in
+ let j = infer env body in
+ let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
let def =
if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
@@ -268,8 +268,7 @@ let record_aux env s_ty s_bo suggested_expr =
let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
let set_suggest_proof_using f = suggest_proof_using := f
-let build_constant_declaration ~flags kn env (def,typ,proj,poly,univs,inline_code,ctx) =
- let flags = { flags with check_universes = flags.check_universes && not (type_in_type env) } in
+let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
let open Context.Named.Declaration in
let check declared inferred =
let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in
@@ -354,7 +353,7 @@ let build_constant_declaration ~flags kn env (def,typ,proj,poly,univs,inline_cod
const_polymorphic = poly;
const_universes = univs;
const_inline_code = inline_code;
- const_typing_flags = flags;
+ const_typing_flags = Environ.typing_flags env;
}
in
let env = add_constant kn cb env in
@@ -369,13 +368,13 @@ let build_constant_declaration ~flags kn env (def,typ,proj,poly,univs,inline_cod
const_polymorphic = poly;
const_universes = univs;
const_inline_code = inline_code;
- const_typing_flags = flags }
+ const_typing_flags = Environ.typing_flags env }
(*s Global and local constant declaration. *)
-let translate_constant ~flags mb env kn ce =
- build_constant_declaration ~flags kn env
- (infer_declaration ~flags ~trust:mb env (Some kn) ce)
+let translate_constant mb env kn ce =
+ build_constant_declaration kn env
+ (infer_declaration ~trust:mb env (Some kn) ce)
let constant_entry_of_side_effect cb u =
let pt =
@@ -410,7 +409,7 @@ type side_effect_role =
type exported_side_effect =
constant * constant_body * side_effects constant_entry * side_effect_role
-let export_side_effects ~flags mb env ce =
+let export_side_effects mb env ce =
match ce with
| ParameterEntry _ | ProjectionEntry _ -> [], ce
| DefinitionEntry c ->
@@ -451,7 +450,7 @@ let export_side_effects ~flags mb env ce =
let env, cbs =
List.fold_left (fun (env,cbs) (kn, ocb, u, r) ->
let ce = constant_entry_of_side_effect ocb u in
- let cb = translate_constant ~flags mb env kn ce in
+ let cb = translate_constant mb env kn ce in
(push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs))
(env,[]) cbs in
translate_seff sl rest (cbs @ acc) env
@@ -466,17 +465,17 @@ let export_side_effects ~flags mb env ce =
translate_seff trusted seff [] env
;;
-let translate_local_assum ~flags env t =
- let j = infer ~flags env t in
+let translate_local_assum env t =
+ let j = infer env t in
let t = Typeops.assumption_of_judgment env j in
t
let translate_recipe env kn r =
- build_constant_declaration ~flags:Declareops.safe_flags kn env (Cooking.cook_constant env r)
+ build_constant_declaration kn env (Cooking.cook_constant env r)
-let translate_local_def ~flags mb env id centry =
+let translate_local_def mb env id centry =
let def,typ,proj,poly,univs,inline_code,ctx =
- infer_declaration ~flags ~trust:mb env None (DefinitionEntry centry) in
+ infer_declaration ~trust:mb env None (DefinitionEntry centry) in
let typ = type_of_constant_type env typ in
if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin
match def with
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index b635f2d31..fcd95576c 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,10 +12,10 @@ open Environ
open Declarations
open Entries
-val translate_local_def : flags:typing_flags -> structure_body -> env -> Id.t -> side_effects definition_entry ->
+val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
constant_def * types * constant_universes
-val translate_local_assum : flags:typing_flags -> env -> types -> types
+val translate_local_assum : env -> types -> types
val mk_pure_proof : constr -> side_effects proof_output
@@ -32,7 +32,7 @@ val inline_entry_side_effects :
val uniq_seff : side_effects -> side_effects
val translate_constant :
- flags:typing_flags -> structure_body -> env -> constant -> side_effects constant_entry ->
+ structure_body -> env -> constant -> side_effects constant_entry ->
constant_body
type side_effect_role =
@@ -47,7 +47,7 @@ type exported_side_effect =
* be pushed in the safe_env by safe typing. The main constant entry
* needs to be translated as usual after this step. *)
val export_side_effects :
- flags:typing_flags -> structure_body -> env -> side_effects constant_entry ->
+ structure_body -> env -> side_effects constant_entry ->
exported_side_effect list * side_effects constant_entry
val constant_entry_of_side_effect :
@@ -60,11 +60,11 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
(** Internal functions, mentioned here for debug purpose only *)
-val infer_declaration : flags:typing_flags -> trust:structure_body -> env -> constant option ->
+val infer_declaration : trust:structure_body -> env -> constant option ->
side_effects constant_entry -> Cooking.result
val build_constant_declaration :
- flags:typing_flags -> constant -> env -> Cooking.result -> constant_body
+ constant -> env -> Cooking.result -> constant_body
val set_suggest_proof_using :
(string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 9b9792ce8..0ea68e2bc 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -500,13 +500,13 @@ let rec execute env cstr =
| Fix ((vn,i as vni),recdef) ->
let (fix_ty,recdef') = execute_recdef env recdef i in
let fix = (vni,recdef') in
- check_fix ~flags:Declareops.safe_flags env fix;
+ check_fix env fix;
make_judge (mkFix fix) fix_ty
| CoFix (i,recdef) ->
let (fix_ty,recdef') = execute_recdef env recdef i in
let cofix = (i,recdef') in
- check_cofix ~flags:Declareops.safe_flags env cofix;
+ check_cofix env cofix;
(make_judge (mkCoFix cofix) fix_ty)
(* Partial proofs: unsupported by the kernel *)
diff --git a/library/declare.ml b/library/declare.ml
index 335263f8f..4e9e68dff 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -58,11 +58,11 @@ let cache_variable ((sp,_),o) =
let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
| SectionLocalAssum ((ty,ctx),poly,impl) ->
- let () = Global.push_named_assum ~flags:Declareops.safe_flags ((id,ty,poly),ctx) in
+ let () = Global.push_named_assum ((id,ty,poly),ctx) in
let impl = if impl then Implicit else Explicit in
impl, true, poly, ctx
| SectionLocalDef (de) ->
- let univs = Global.push_named_def ~flags:Declareops.safe_flags (id,de) in
+ let univs = Global.push_named_def (id,de) in
Explicit, de.const_entry_opaque,
de.const_entry_polymorphic, univs in
Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
@@ -180,7 +180,7 @@ let discharge_constant ((sp, kn), obj) =
(* Hack to reduce the size of .vo: we keep only what load/open needs *)
let dummy_constant_entry =
ConstantEntry
- (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), Declareops.safe_flags)
+ (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
let dummy_constant cst = {
cst_decl = dummy_constant_entry;
@@ -205,7 +205,7 @@ let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) =
let declare_scheme = ref (fun _ _ -> assert false)
let set_declare_scheme f = declare_scheme := f
-let declare_constant_common ~flags id cst =
+let declare_constant_common id cst =
let update_tables c =
(* Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *)
declare_constant_implicits c;
@@ -216,7 +216,7 @@ let declare_constant_common ~flags id cst =
List.iter (fun (c,ce,role) ->
(* handling of private_constants just exported *)
let o = inConstant {
- cst_decl = ConstantEntry (false, ce, flags);
+ cst_decl = ConstantEntry (false, ce);
cst_hyps = [] ;
cst_kind = IsProof Theorem;
cst_locl = false;
@@ -246,7 +246,7 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
const_entry_feedback = None;
const_entry_inline_code = inline}
-let declare_constant ?(flags=Declareops.safe_flags) ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
+let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
let export = (* We deal with side effects *)
match cd with
| DefinitionEntry de when
@@ -259,24 +259,24 @@ let declare_constant ?(flags=Declareops.safe_flags) ?(internal = UserIndividualR
| _ -> false
in
let cst = {
- cst_decl = ConstantEntry (export,cd,flags);
+ cst_decl = ConstantEntry (export,cd);
cst_hyps = [] ;
cst_kind = kind;
cst_locl = local;
cst_exported = [];
cst_was_seff = false;
} in
- let kn = declare_constant_common id cst ~flags in
+ let kn = declare_constant_common id cst in
let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in
kn
-let declare_definition ?flags ?(internal=UserIndividualRequest)
+let declare_definition ?(internal=UserIndividualRequest)
?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
?(poly=false) id ?types (body,ctx) =
let cb =
definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
in
- declare_constant ?flags ~internal ~local id
+ declare_constant ~internal ~local id
(Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
(** Declaration of inductive blocks *)
@@ -374,7 +374,7 @@ let declare_projections mind =
Array.iteri (fun i kn ->
let id = Label.to_id (Constant.label kn) in
let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
- let kn' = declare_constant ~flags:Declareops.safe_flags id (ProjectionEntry entry,
+ let kn' = declare_constant id (ProjectionEntry entry,
IsDefinition StructureComponent)
in
assert(eq_constant kn kn')) kns; true,true
diff --git a/library/declare.mli b/library/declare.mli
index 41221d5c9..8dd24d278 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -54,11 +54,9 @@ val definition_entry : ?fix_exn:Future.fix_exn ->
?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
val declare_constant :
- ?flags:Declarations.typing_flags -> (** default Declareops.safe_flags *)
?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
val declare_definition :
- ?flags:Declarations.typing_flags -> (** default Declareops.safe_flags *)
?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr ->
constr Univ.in_universe_context_set -> constant
diff --git a/library/global.ml b/library/global.ml
index e456841f8..c53611931 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -77,13 +77,14 @@ let globalize_with_summary fs f =
let i2l = Label.of_id
-let push_named_assum ~flags a = globalize0 (Safe_typing.push_named_assum ~flags a)
-let push_named_def ~flags d = globalize (Safe_typing.push_named_def ~flags d)
+let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
+let push_named_def d = globalize (Safe_typing.push_named_def d)
let add_constraints c = globalize0 (Safe_typing.add_constraints c)
let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
let push_context b c = globalize0 (Safe_typing.push_context b c)
let set_engagement c = globalize0 (Safe_typing.set_engagement c)
+let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
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 91fc55918..247ca20b4 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -27,11 +27,12 @@ val named_context : unit -> Context.Named.t
(** Changing the (im)predicativity of the system *)
val set_engagement : Declarations.engagement -> unit
+val set_typing_flags : Declarations.typing_flags -> unit
(** Variables, Local definitions, constants, inductive types *)
-val push_named_assum : flags:Declarations.typing_flags -> (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
-val push_named_def : flags:Declarations.typing_flags -> (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set
+val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
+val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set
val add_constant :
DirPath.t -> Id.t -> Safe_typing.global_declaration ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 8b3d3dc20..0cacb003d 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -400,7 +400,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
in
evd,List.rev rev_pconstants
| _ ->
- Command.do_fixpoint ~flags:Declareops.safe_flags Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
+ Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
let evd,rev_pconstants =
List.fold_left
(fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1d7720454..403dcfd1a 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -592,9 +592,9 @@ let type_of_projection_knowing_arg env sigma p c ty =
let control_only_guard env c =
let check_fix_cofix e c = match kind_of_term c with
| CoFix (_,(_,_,_) as cofix) ->
- Inductive.check_cofix ~flags:Declareops.safe_flags e cofix
+ Inductive.check_cofix e cofix
| Fix (_,(_,_,_) as fix) ->
- Inductive.check_fix ~flags:Declareops.safe_flags e fix
+ Inductive.check_fix e fix
| _ -> ()
in
let rec iter env c =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 65f5b3fd0..b6a57785a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -72,17 +72,14 @@ open Inductiveops
exception Found of int array
-(* spiwack: I chose [tflags] rather than [flags], like in the rest of
- the code, for the argument name to avoid interference with the
- argument for [inference_flags] also used in this module. *)
-let search_guard ~tflags loc env possible_indexes fixdefs =
+let search_guard loc env possible_indexes fixdefs =
(* Standard situation with only one possibility for each fix. *)
(* We treat it separately in order to get proper error msg. *)
let is_singleton = function [_] -> true | _ -> false in
if List.for_all is_singleton possible_indexes then
let indexes = Array.of_list (List.map List.hd possible_indexes) in
let fix = ((indexes, 0),fixdefs) in
- (try check_fix env ~flags:tflags fix
+ (try check_fix env fix
with reraise ->
let (e, info) = Errors.push reraise in
let info = Loc.add_loc info loc in
@@ -101,7 +98,10 @@ let search_guard ~tflags loc env possible_indexes fixdefs =
will be chosen). A more robust solution may be to raise an
error when totality is assumed but the strutural argument is
not specified. *)
- try check_fix env ~flags:Declareops.safe_flags fix; raise (Found indexes)
+ try
+ let flags = { (typing_flags env) with Declarations.check_guarded = true } in
+ let env = Environ.set_typing_flags flags env in
+ check_fix env fix; raise (Found indexes)
with TypeError _ -> ())
(List.combinations possible_indexes);
let errmsg = "Cannot guess decreasing argument of fix." in
@@ -617,13 +617,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
let fixdecls = (names,ftys,fdefs) in
let indexes =
search_guard
- ~tflags:Declareops.safe_flags
loc env possible_indexes fixdecls
in
make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
| GCoFix i ->
let cofix = (i,(names,ftys,fdefs)) in
- (try check_cofix env ~flags:Declareops.safe_flags cofix
+ (try check_cofix env cofix
with reraise ->
let (e, info) = Errors.push reraise in
let info = Loc.add_loc info loc in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 2c02b4a21..824bb11aa 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -22,7 +22,7 @@ open Misctypes
(** An auxiliary function for searching for fixpoint guard indexes *)
-val search_guard : tflags:Declarations.typing_flags ->
+val search_guard :
Loc.t -> env -> int list list -> rec_declaration -> int array
type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index f03e6c6e9..52afa7f83 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -189,13 +189,13 @@ let rec execute env evdref cstr =
| Fix ((vn,i as vni),recdef) ->
let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
let fix = (vni,recdef') in
- check_fix env ~flags:Declareops.safe_flags fix;
+ check_fix env fix;
make_judge (mkFix fix) tys.(i)
| CoFix (i,recdef) ->
let (_,tys,_ as recdef') = execute_recdef env evdref recdef in
let cofix = (i,recdef') in
- check_cofix env ~flags:Declareops.safe_flags cofix;
+ check_cofix env cofix;
make_judge (mkCoFix cofix) tys.(i)
| Sort (Prop c) ->
diff --git a/printing/printer.ml b/printing/printer.ml
index 509e982dc..8af2af98a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -775,7 +775,7 @@ module ContextObjectMap = Map.Make (OrderedContextObject)
let pr_assumptionset env s =
if ContextObjectMap.is_empty s &&
- engagement env = (PredicativeSet, StratifiedType) then
+ engagement env = PredicativeSet then
str "Closed under the global context"
else
let safe_pr_constant env kn =
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 6d84219d9..39f581082 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -79,7 +79,7 @@ let adjust_guardness_conditions const = function
List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l)
env (Safe_typing.side_effects_of_private_constants eff) in
let indexes =
- search_guard ~tflags:Declareops.safe_flags Loc.ghost env
+ search_guard Loc.ghost env
possible_indexes fixdecls in
(mkFix ((indexes,0),fixdecls), ctx), eff
| _ -> (body, ctx), eff) }
diff --git a/toplevel/command.ml b/toplevel/command.ml
index ff43cd495..643b06660 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -145,9 +145,9 @@ let get_locality id = function
| Local -> true
| Global -> false
-let declare_global_definition ~flags ident ce local k pl imps =
+let declare_global_definition ident ce local k pl imps =
let local = get_locality ident local in
- let kn = declare_constant ~flags ident ~local (DefinitionEntry ce, IsDefinition k) in
+ let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
let gr = ConstRef kn in
let () = maybe_declare_manual_implicits false gr imps in
let () = Universes.register_universe_binders gr pl in
@@ -158,7 +158,7 @@ let declare_definition_hook = ref ignore
let set_declare_definition_hook = (:=) declare_definition_hook
let get_declare_definition_hook () = !declare_definition_hook
-let declare_definition ~flags ident (local, p, k) ce pl imps hook =
+let declare_definition ident (local, p, k) ce pl imps hook =
let fix_exn = Future.fix_exn_of ce.const_entry_body in
let () = !declare_definition_hook ce in
let r = match local with
@@ -175,11 +175,11 @@ let declare_definition ~flags ident (local, p, k) ce pl imps hook =
in
gr
| Discharge | Local | Global ->
- declare_global_definition ~flags ident ce local k pl imps in
+ declare_global_definition ident ce local k pl imps in
Lemmas.call_hook fix_exn hook local r
let _ = Obligations.declare_definition_ref :=
- (fun i k c imps hook -> declare_definition ~flags:Declareops.safe_flags i k c [] imps hook)
+ (fun i k c imps hook -> declare_definition i k c [] imps hook)
let do_definition ident k pl bl red_option c ctypopt hook =
let (ce, evd, pl', imps as def) =
@@ -203,7 +203,7 @@ let do_definition ident k pl bl red_option c ctypopt hook =
ignore(Obligations.add_definition
ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls)
else let ce = check_definition def in
- ignore(declare_definition ~flags:Declareops.safe_flags ident k ce pl' imps
+ ignore(declare_definition ident k ce pl' imps
(Lemmas.mk_hook
(fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
@@ -833,12 +833,12 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
-let declare_fix ~flags ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
+let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
- declare_definition ~flags f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
+ declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
let _ = Obligations.declare_fix_ref :=
- (fun ?opaque k ctx f d t imps -> declare_fix ~flags:Declareops.safe_flags ?opaque k [] ctx f d t imps)
+ (fun ?opaque k ctx f d t imps -> declare_fix ?opaque k [] ctx f d t imps)
let prepare_recursive_declaration fixnames fixtypes fixdefs =
let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
@@ -1139,7 +1139,7 @@ let interp_cofixpoint l ntns =
check_recursive false env evd fix;
(fix,pl,Evd.evar_universe_context evd,info)
-let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
@@ -1159,7 +1159,7 @@ let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fixim
let fixdefs = List.map Option.get fixdefs in
let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
let env = Global.env() in
- let indexes = search_guard ~tflags:flags Loc.ghost env indexes fixdecls in
+ let indexes = search_guard Loc.ghost env indexes fixdecls in
let fiximps = List.map (fun (n,r,p) -> r) fiximps in
let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
let fixdecls =
@@ -1168,7 +1168,7 @@ let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fixim
let evd = Evd.restrict_universe_context evd vars in
let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
let pl, ctx = Evd.universe_context ?names:pl evd in
- ignore (List.map4 (declare_fix ~flags (local, poly, Fixpoint) pl ctx)
+ ignore (List.map4 (declare_fix (local, poly, Fixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
fixpoint_message (Some indexes) fixnames;
@@ -1176,7 +1176,7 @@ let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fixim
(* Declare notations *)
List.iter Metasyntax.add_notation_interpretation ntns
-let declare_cofixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
if List.exists Option.is_empty fixdefs then
(* Some bodies to define by proof *)
let thms =
@@ -1202,7 +1202,7 @@ let declare_cofixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fix
let evd = Evd.from_ctx ctx in
let evd = Evd.restrict_universe_context evd vars in
let pl, ctx = Evd.universe_context ?names:pl evd in
- ignore (List.map4 (declare_fix ~flags (local, poly, CoFixpoint) pl ctx)
+ ignore (List.map4 (declare_fix (local, poly, CoFixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
cofixpoint_message fixnames
@@ -1269,11 +1269,9 @@ let do_program_recursive local p fixkind fixl ntns =
in
let indexes =
Pretyping.search_guard
- ~tflags:Declareops.safe_flags
Loc.ghost (Global.env ()) possible_indexes fixdecls in
List.iteri (fun i _ ->
Inductive.check_fix env
- ~flags:Declareops.safe_flags
((indexes,i),fixdecls))
fixl
end in
@@ -1309,21 +1307,26 @@ let do_program_fixpoint local poly l =
errorlabstrm "do_program_fixpoint"
(str "Well-founded fixpoints not allowed in mutually recursive blocks")
-let do_fixpoint ~flags local poly l =
+let check_safe () =
+ let open Declarations in
+ let flags = Environ.typing_flags (Global.env ()) in
+ flags.check_universes && flags.check_guarded
+
+let do_fixpoint local poly l =
if Flags.is_program_mode () then do_program_fixpoint local poly l
else
let fixl, ntns = extract_fixpoint_components true l in
let (_, _, _, info as fix) = interp_fixpoint fixl ntns in
let possible_indexes =
List.map compute_possible_guardness_evidences info in
- declare_fixpoint ~flags local poly fix possible_indexes ntns;
- if not flags.Declarations.check_guarded then Feedback.feedback Feedback.AddedAxiom else ()
+ declare_fixpoint local poly fix possible_indexes ntns;
+ if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
-let do_cofixpoint ~flags local poly l =
+let do_cofixpoint local poly l =
let fixl,ntns = extract_cofixpoint_components l in
if Flags.is_program_mode () then
do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns
else
let cofix = interp_cofixpoint fixl ntns in
- declare_cofixpoint ~flags local poly cofix ntns;
- if not flags.Declarations.check_guarded then Feedback.feedback Feedback.AddedAxiom else ()
+ declare_cofixpoint local poly cofix ntns;
+ if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 2d27552a1..a5132cc66 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -36,7 +36,7 @@ val interp_definition :
constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map *
Universes.universe_binders * Impargs.manual_implicits
-val declare_definition : flags:Declarations.typing_flags -> Id.t -> definition_kind ->
+val declare_definition : Id.t -> definition_kind ->
Safe_typing.private_constants definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
@@ -150,13 +150,12 @@ val interp_cofixpoint :
(** Registering fixpoints and cofixpoints in the environment *)
val declare_fixpoint :
- flags:Declarations.typing_flags ->
locality -> polymorphic ->
recursive_preentry * lident list option * Evd.evar_universe_context *
(Name.t list * Impargs.manual_implicits * int option) list ->
lemma_possible_guards -> decl_notation list -> unit
-val declare_cofixpoint : flags:Declarations.typing_flags -> locality -> polymorphic ->
+val declare_cofixpoint : locality -> polymorphic ->
recursive_preentry * lident list option * Evd.evar_universe_context *
(Name.t list * Impargs.manual_implicits * int option) list ->
decl_notation list -> unit
@@ -164,16 +163,16 @@ val declare_cofixpoint : flags:Declarations.typing_flags -> locality -> polymorp
(** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
val do_fixpoint :
- flags:Declarations.typing_flags -> (* When [false], assume guarded. *)
+ (* When [false], assume guarded. *)
locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
val do_cofixpoint :
- flags:Declarations.typing_flags -> (* When [false], assume guarded. *)
+ (* When [false], assume guarded. *)
locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
(** Utils *)
val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
-val declare_fix : flags:Declarations.typing_flags -> ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
+val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 46fb55b5f..e34f38eb3 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -115,10 +115,11 @@ let _ = at_exit print_memory_stat
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 set_type_in_type () =
+ let typing_flags = Environ.typing_flags (Global.env ()) in
+ Global.set_typing_flags { typing_flags with Declarations.check_universes = false }
let engage () =
- Global.set_engagement (!impredicative_set,!type_in_type)
+ Global.set_engagement !impredicative_set
let set_batch_mode () = batch_mode := true
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 3d15f2142..4d8d537f2 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -567,7 +567,7 @@ let declare_mutual_definition l =
List.map3 compute_possible_guardness_evidences
wfl fixdefs fixtypes in
let indexes =
- Pretyping.search_guard ~tflags:Declareops.safe_flags
+ Pretyping.search_guard
Loc.ghost (Global.env())
possible_indexes fixdecls in
Some indexes,
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5131a4179..29d6d7acd 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -576,17 +576,17 @@ let vernac_inductive chk poly lo finite indl =
let indl = List.map unpack indl in
do_mutual_inductive chk indl poly lo finite
-let vernac_fixpoint ~flags locality poly local l =
+let vernac_fixpoint locality poly local l =
let local = enforce_locality_exp locality local in
if Dumpglob.dump () then
List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
- do_fixpoint ~flags local poly l
+ do_fixpoint local poly l
-let vernac_cofixpoint ~flags locality poly local l =
+let vernac_cofixpoint locality poly local l =
let local = enforce_locality_exp locality local in
if Dumpglob.dump () then
List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
- do_cofixpoint ~flags local poly l
+ do_cofixpoint local poly l
let vernac_scheme l =
if Dumpglob.dump () then
@@ -1731,8 +1731,6 @@ let vernac_load interp fname =
try while true do interp (snd (parse_sentence input)) done
with End_of_input -> ()
-let all_checks = Declareops.safe_flags
-
(* "locality" is the prefix "Local" attribute, while the "local" component
* is the outdated/deprecated "Local" attribute of some vernacular commands
* still parsed as the obsolete_locality grammar entry for retrocompatibility.
@@ -1770,8 +1768,8 @@ let interp ?proof ~loc locality poly c =
| VernacExactProof c -> vernac_exact_proof c
| VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
| VernacInductive (priv,finite,l) -> vernac_inductive true poly priv finite l
- | VernacFixpoint (local, l) -> vernac_fixpoint locality ~flags:all_checks poly local l
- | VernacCoFixpoint (local, l) -> vernac_cofixpoint ~flags:all_checks locality poly local l
+ | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l
+ | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
| VernacScheme l -> vernac_scheme l
| VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
| VernacUniverse l -> vernac_universe loc poly l
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 22:06:03 +0000