aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/fast_typeops.ml69
-rw-r--r--kernel/fast_typeops.mli6
-rw-r--r--kernel/safe_typing.ml13
-rw-r--r--kernel/safe_typing.mli4
-rw-r--r--kernel/term_typing.ml28
-rw-r--r--kernel/term_typing.mli8
-rw-r--r--library/declare.ml18
-rw-r--r--library/declare.mli2
-rw-r--r--library/global.ml4
-rw-r--r--library/global.mli6
-rw-r--r--toplevel/command.ml22
-rw-r--r--toplevel/command.mli7
12 files changed, 100 insertions, 87 deletions
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 358795666..8c14f5e04 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -326,7 +326,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 env cstr =
+let rec execute ~chkguard env cstr =
match kind_of_term cstr with
(* Atomic terms *)
| Sort (Prop c) ->
@@ -345,12 +345,12 @@ let rec execute env cstr =
judge_of_constant env c
| Proj (p, c) ->
- let ct = execute env c in
+ let ct = execute ~chkguard env c in
judge_of_projection env p c ct
(* Lambda calculus operators *)
| App (f,args) ->
- let argst = execute_array env args in
+ let argst = execute_array ~chkguard env args in
let ft =
match kind_of_term f with
| Ind ind when Environ.template_polymorphic_pind ind env ->
@@ -363,7 +363,7 @@ let rec execute env cstr =
judge_of_constant_knowing_parameters env cst args
| _ ->
(* Full or no sort-polymorphism *)
- execute env f
+ execute ~chkguard env f
in
judge_of_apply env f ft args argst
@@ -371,25 +371,25 @@ let rec execute env cstr =
| Lambda (name,c1,c2) ->
let _ = execute_is_type env c1 in
let env1 = push_rel (name,None,c1) env in
- let c2t = execute env1 c2 in
+ let c2t = execute ~chkguard env1 c2 in
judge_of_abstraction env name c1 c2t
| Prod (name,c1,c2) ->
- let vars = execute_is_type env c1 in
+ let vars = execute_is_type ~chkguard env c1 in
let env1 = push_rel (name,None,c1) env in
- let vars' = execute_is_type env1 c2 in
+ let vars' = execute_is_type ~chkguard env1 c2 in
judge_of_product env name vars vars'
| LetIn (name,c1,c2,c3) ->
- let c1t = execute env c1 in
+ let c1t = execute ~chkguard 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 (name,Some c1,c2) env in
- let c3t = execute env1 c3 in
+ let c3t = execute ~chkguard env1 c3 in
subst1 c1 c3t
| Cast (c,k,t) ->
- let ct = execute env c in
+ let ct = execute ~chkguard env c in
let _ts = execute_type env t in
let _ = judge_of_cast env c ct k t in
t
@@ -402,20 +402,20 @@ let rec execute env cstr =
judge_of_constructor env c
| Case (ci,p,c,lf) ->
- let ct = execute env c in
- let pt = execute env p in
- let lft = execute_array env lf in
+ let ct = execute ~chkguard env c in
+ let pt = execute ~chkguard env p in
+ let lft = execute_array ~chkguard 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 env recdef i in
+ let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in
let fix = (vni,recdef') in
- check_fix env ~chk:true fix; fix_ty
+ check_fix env ~chk:chkguard fix; fix_ty
| CoFix (i,recdef) ->
- let (fix_ty,recdef') = execute_recdef env recdef i in
+ let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in
let cofix = (i,recdef') in
- check_cofix env ~chk:true cofix; fix_ty
+ check_cofix env ~chk:chkguard cofix; fix_ty
(* Partial proofs: unsupported by the kernel *)
| Meta _ ->
@@ -424,38 +424,41 @@ let rec execute env cstr =
| Evar _ ->
anomaly (Pp.str "the kernel does not support existential variables")
-and execute_is_type env constr =
- let t = execute env constr in
+and execute_is_type ~chkguard env constr =
+ let t = execute ~chkguard env constr in
check_type env constr t
-and execute_type env constr =
- let t = execute env constr in
+and execute_type ~chkguard env constr =
+ let t = execute ~chkguard env constr in
type_judgment env constr t
-and execute_recdef env (names,lar,vdef) i =
- let lart = execute_array env lar in
+and execute_recdef ~chkguard env (names,lar,vdef) i =
+ let lart = execute_array ~chkguard 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 env1 vdef in
+ let vdeft = execute_array ~chkguard env1 vdef in
let () = type_fixpoint env1 names lara vdef vdeft in
(lara.(i),(names,lara,vdef))
-and execute_array env = Array.map (execute env)
+and execute_array ~chkguard env = Array.map (execute ~chkguard env)
(* Derived functions *)
-let infer env constr =
- let t = execute env constr in
+let infer ~chkguard env constr =
+ let t = execute ~chkguard env constr in
make_judge constr t
let infer =
if Flags.profile then
let infer_key = Profile.declare_profile "Fast_infer" in
- Profile.profile2 infer_key infer
- else infer
+ Profile.profile3 infer_key (fun a b c -> infer ~chkguard:a b c)
+ else (fun a b c -> infer ~chkguard:a b c)
-let infer_type env constr =
- execute_type env constr
+(* Restores the labels of [infer] lost to profiling. *)
+let infer ~chkguard env t = infer chkguard env t
-let infer_v env cv =
- let jv = execute_array env cv in
+let infer_type ~chkguard env constr =
+ execute_type ~chkguard env constr
+
+let infer_v ~chkguard env cv =
+ let jv = execute_array ~chkguard env cv in
make_judgev cv jv
diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli
index 90d9c55f1..98dbefad1 100644
--- a/kernel/fast_typeops.mli
+++ b/kernel/fast_typeops.mli
@@ -18,6 +18,6 @@ open Environ
*)
-val infer : env -> constr -> unsafe_judgment
-val infer_v : env -> constr array -> unsafe_judgment array
-val infer_type : env -> types -> unsafe_type_judgment
+val infer : chkguard:bool -> env -> constr -> unsafe_judgment
+val infer_v : chkguard:bool -> env -> constr array -> unsafe_judgment array
+val infer_type : chkguard:bool -> env -> types -> unsafe_type_judgment
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d9adca0c9..18d897817 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -332,8 +332,8 @@ let safe_push_named (id,_,_ as d) env =
Environ.push_named d env
-let push_named_def (id,de) senv =
- let c,typ,univs = Term_typing.translate_local_def senv.env id de in
+let push_named_def ~chkguard (id,de) senv =
+ let c,typ,univs = Term_typing.translate_local_def ~chkguard senv.env id de in
let senv' = push_context univs senv in
let c, senv' = match c with
| Def c -> Mod_subst.force_constr c, senv'
@@ -346,9 +346,9 @@ let push_named_def (id,de) senv =
let env'' = safe_push_named (id,Some c,typ) senv'.env in
{senv' with env=env''}
-let push_named_assum ((id,t),ctx) senv =
+let push_named_assum ~chkguard ((id,t),ctx) senv =
let senv' = push_context_set ctx senv in
- let t = Term_typing.translate_local_assum senv'.env t in
+ let t = Term_typing.translate_local_assum ~chkguard senv'.env t in
let env'' = safe_push_named (id,None,t) senv'.env in
{senv' with env=env''}
@@ -439,13 +439,14 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver }
(** Insertion of constants and parameters in environment *)
type global_declaration =
- | ConstantEntry of Entries.constant_entry
+ | ConstantEntry of Entries.constant_entry * bool (* check guard *)
| GlobalRecipe of Cooking.recipe
let add_constant dir l decl senv =
let kn = make_con senv.modpath dir l in
let cb = match decl with
- | ConstantEntry ce -> Term_typing.translate_constant senv.env kn ce
+ | ConstantEntry (ce,chkguard) ->
+ Term_typing.translate_constant ~chkguard senv.env kn ce
| GlobalRecipe r ->
let cb = Term_typing.translate_recipe senv.env kn r in
if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index a57fb108c..80b9bb495 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -57,14 +57,16 @@ val is_joined_environment : safe_environment -> bool
(** Insertion of local declarations (Local or Variables) *)
val push_named_assum :
+ chkguard:bool ->
(Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0
val push_named_def :
+ chkguard:bool ->
Id.t * Entries.definition_entry -> safe_transformer0
(** Insertion of global axioms or definitions *)
type global_declaration =
- | ConstantEntry of Entries.constant_entry
+ | ConstantEntry of Entries.constant_entry * bool (* chkguard *)
| GlobalRecipe of Cooking.recipe
val add_constant :
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a316b4492..539305ed1 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -23,18 +23,18 @@ open Entries
open Typeops
open Fast_typeops
-let constrain_type env j poly subst = function
+let constrain_type ~chkguard 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 env t in
+ let tj = infer_type ~chkguard 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 env t in
+ let tj = infer_type ~chkguard 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)
@@ -101,11 +101,11 @@ let hcons_j j =
let feedback_completion_typecheck =
Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
-let infer_declaration env kn dcl =
+let infer_declaration ~chkguard env kn dcl =
match dcl with
| ParameterEntry (ctx,poly,(t,uctx),nl) ->
let env = push_context uctx env in
- let j = infer env t in
+ let j = infer ~chkguard 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
@@ -122,7 +122,7 @@ let infer_declaration env kn dcl =
Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) ->
let body = handle_side_effects env body side_eff in
let env' = push_context_set ctx env in
- let j = infer env' body in
+ let j = infer ~chkguard env' body in
let j = hcons_j j in
let subst = Univ.LMap.empty in
let _typ = constrain_type env' j c.const_entry_polymorphic subst
@@ -143,8 +143,8 @@ let infer_declaration env kn dcl =
let body = handle_side_effects env body side_eff in
let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in
- let j = infer env body in
- let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
+ let j = infer ~chkguard env body in
+ let typ = constrain_type ~chkguard 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)))
@@ -266,20 +266,20 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
(*s Global and local constant declaration. *)
-let translate_constant env kn ce =
- build_constant_declaration kn env (infer_declaration env (Some kn) ce)
+let translate_constant ~chkguard env kn ce =
+ build_constant_declaration kn env (infer_declaration ~chkguard env (Some kn) ce)
-let translate_local_assum env t =
- let j = infer env t in
+let translate_local_assum ~chkguard env t =
+ let j = infer ~chkguard env t in
let t = Typeops.assumption_of_judgment env j in
t
let translate_recipe env kn r =
build_constant_declaration kn env (Cooking.cook_constant env r)
-let translate_local_def env id centry =
+let translate_local_def ~chkguard env id centry =
let def,typ,proj,poly,univs,inline_code,ctx =
- infer_declaration env None (DefinitionEntry centry) in
+ infer_declaration ~chkguard env None (DefinitionEntry centry) in
let typ = type_of_constant_type env typ in
def, typ, univs
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 1b54b1ea1..a71587f0f 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 : env -> Id.t -> definition_entry ->
+val translate_local_def : chkguard:bool -> env -> Id.t -> definition_entry ->
constant_def * types * constant_universes
-val translate_local_assum : env -> types -> types
+val translate_local_assum : chkguard:bool -> env -> types -> types
val mk_pure_proof : constr -> proof_output
@@ -28,7 +28,7 @@ val handle_entry_side_effects : env -> definition_entry -> definition_entry
{!Entries.const_entry_body} field. It is meant to get a term out of a not
yet type checked proof. *)
-val translate_constant : env -> constant -> constant_entry -> constant_body
+val translate_constant : chkguard:bool -> env -> constant -> constant_entry -> constant_body
val translate_mind :
env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
@@ -37,7 +37,7 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
(** Internal functions, mentioned here for debug purpose only *)
-val infer_declaration : env -> constant option ->
+val infer_declaration : chkguard:bool -> env -> constant option ->
constant_entry -> Cooking.result
val build_constant_declaration :
diff --git a/library/declare.ml b/library/declare.ml
index 02e6dadde..4be13109a 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -50,11 +50,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 ((id,ty),ctx) in
+ let () = Global.push_named_assum ~chkguard:true ((id,ty),ctx) in
let impl = if impl then Implicit else Explicit in
impl, true, poly, ctx
| SectionLocalDef (de) ->
- let () = Global.push_named_def (id,de) in
+ let () = Global.push_named_def ~chkguard:true (id,de) in
Explicit, de.const_entry_opaque, de.const_entry_polymorphic,
(Univ.ContextSet.of_context de.const_entry_universes) in
Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
@@ -156,7 +156,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 (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
+ ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), true)
let dummy_constant cst = {
cst_decl = dummy_constant_entry;
@@ -232,7 +232,7 @@ let declare_sideff env fix_exn se =
const_entry_feedback = None;
const_entry_polymorphic = cb.const_polymorphic;
const_entry_universes = univs;
- });
+ }, true);
cst_hyps = [] ;
cst_kind = Decl_kinds.IsDefinition Decl_kinds.Definition;
cst_locl = true;
@@ -253,7 +253,7 @@ let declare_sideff env fix_exn se =
if Constant.equal c c' then Some (x,kn) else None) inds_consts)
knl))
-let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
+let declare_constant ?(chkguard=true) ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
let cd = (* We deal with side effects *)
match cd with
| Entries.DefinitionEntry de ->
@@ -275,7 +275,7 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff
| _ -> cd
in
let cst = {
- cst_decl = ConstantEntry cd;
+ cst_decl = ConstantEntry (cd,chkguard);
cst_hyps = [] ;
cst_kind = kind;
cst_locl = local;
@@ -283,13 +283,13 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff
let kn = declare_constant_common id cst in
kn
-let declare_definition ?(internal=UserVerbose)
+let declare_definition ?chkguard ?(internal=UserVerbose)
?(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 ~internal ~local id
+ declare_constant ?chkguard ~internal ~local id
(Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
(** Declaration of inductive blocks *)
@@ -387,7 +387,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 id (ProjectionEntry entry,
+ let kn' = declare_constant ~chkguard:true id (ProjectionEntry entry,
IsDefinition StructureComponent)
in
assert(eq_constant kn kn')) kns; true
diff --git a/library/declare.mli b/library/declare.mli
index d8a00db0c..94cebe3bd 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -53,9 +53,11 @@ val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types ->
constr -> definition_entry
val declare_constant :
+ ?chkguard:bool -> (** default [true] (check guardedness) *)
?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
val declare_definition :
+ ?chkguard:bool -> (** default [true] (check guardedness) *)
?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 49fa2ef28..27f7f5266 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -77,8 +77,8 @@ let globalize_with_summary fs f =
let i2l = Label.of_id
-let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
-let push_named_def d = globalize0 (Safe_typing.push_named_def d)
+let push_named_assum ~chkguard a = globalize0 (Safe_typing.push_named_assum ~chkguard a)
+let push_named_def ~chkguard d = globalize0 (Safe_typing.push_named_def ~chkguard d)
let add_constraints c = globalize0 (Safe_typing.add_constraints c)
let push_context_set c = globalize0 (Safe_typing.push_context_set c)
let push_context c = globalize0 (Safe_typing.push_context c)
diff --git a/library/global.mli b/library/global.mli
index 248e1f86d..388fee527 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -31,8 +31,10 @@ val set_type_in_type : unit -> unit
(** Variables, Local definitions, constants, inductive types *)
-val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit
-val push_named_def : (Id.t * Entries.definition_entry) -> unit
+val push_named_assum :
+ chkguard:bool -> (Id.t * Constr.types) Univ.in_universe_context_set -> unit
+val push_named_def :
+ chkguard:bool -> (Id.t * Entries.definition_entry) -> unit
val add_constant :
DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 14a1efe4d..ac46b439c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -139,9 +139,9 @@ let get_locality id = function
| Local -> true
| Global -> false
-let declare_global_definition ident ce local k imps =
+let declare_global_definition ~chkguard ident ce local k imps =
let local = get_locality ident local in
- let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
+ let kn = declare_constant ~chkguard ident ~local (DefinitionEntry ce, IsDefinition k) in
let gr = ConstRef kn in
let () = maybe_declare_manual_implicits false gr imps in
let () = definition_message ident in
@@ -151,7 +151,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 ident (local, p, k) ce imps hook =
+let declare_definition ~chkguard ident (local, p, k) ce imps hook =
let () = !declare_definition_hook ce in
let r = match local with
| Discharge when Lib.sections_are_opened () ->
@@ -167,10 +167,10 @@ let declare_definition ident (local, p, k) ce imps hook =
in
gr
| Discharge | Local | Global ->
- declare_global_definition ident ce local k imps in
+ declare_global_definition ~chkguard ident ce local k imps in
Lemmas.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r
-let _ = Obligations.declare_definition_ref := declare_definition
+let _ = Obligations.declare_definition_ref := declare_definition ~chkguard:true
let do_definition ident k bl red_option c ctypopt hook =
let (ce, evd, imps as def) = interp_definition bl (pi2 k) red_option c ctypopt in
@@ -191,7 +191,7 @@ let do_definition ident k bl red_option c ctypopt hook =
ignore(Obligations.add_definition
ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
else let ce = check_definition def in
- ignore(declare_definition ident k ce imps
+ ignore(declare_definition ~chkguard:true ident k ce imps
(Lemmas.mk_hook
(fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
@@ -752,11 +752,11 @@ 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 ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
+let declare_fix ~chkguard ?(opaque = false) (_,poly,_ as kind) ctx f ((def,_),eff) t imps =
let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
- declare_definition f kind ce imps (Lemmas.mk_hook (fun _ r -> r))
+ declare_definition ~chkguard f kind ce imps (Lemmas.mk_hook (fun _ r -> r))
-let _ = Obligations.declare_fix_ref := declare_fix
+let _ = Obligations.declare_fix_ref := (declare_fix ~chkguard:true)
let prepare_recursive_declaration fixnames fixtypes fixdefs =
let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
@@ -1072,7 +1072,7 @@ let declare_fixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fixim
let ctx = Universes.restrict_universe_context ctx vars in
let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
let ctx = Univ.ContextSet.to_context ctx in
- ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx)
+ ignore (List.map4 (declare_fix ~chkguard (local, poly, Fixpoint) ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
fixpoint_message (Some indexes) fixnames;
@@ -1103,7 +1103,7 @@ let declare_cofixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fix
let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in
let ctx = Univ.ContextSet.to_context ctx in
- ignore (List.map4 (declare_fix (local, poly, CoFixpoint) ctx)
+ ignore (List.map4 (declare_fix ~chkguard (local, poly, CoFixpoint) ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
cofixpoint_message fixnames
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 7112591fe..7578e26c1 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -34,7 +34,8 @@ val interp_definition :
local_binder list -> polymorphic -> red_expr option -> constr_expr ->
constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
-val declare_definition : Id.t -> definition_kind ->
+val declare_definition : chkguard:bool ->
+ Id.t -> definition_kind ->
definition_entry -> Impargs.manual_implicits ->
Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
@@ -172,5 +173,7 @@ val do_cofixpoint :
val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
-val declare_fix : ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
+val declare_fix :
+ chkguard:bool ->
+ ?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t ->
Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 19:17:15 +0000