diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2015-07-24 08:46:09 +0200 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-09-25 10:41:41 +0200 |
commit | e8bad8abc7be351a34fdf9770409bbab14bcd6a9 (patch) | |
tree | 00ca0103024f39e5943dcce5a89e9283708ae323 | |
parent | 8f64e84a3560bcf668b00ac93ab33542456a9bda (diff) |
Propagate `Guarded` flag from syntax to kernel.
The path is quite a bit of a maze, this commit is not as simple as it ought to be. Something more robust than a boolean should be used here.
-rw-r--r-- | kernel/fast_typeops.ml | 69 | ||||
-rw-r--r-- | kernel/fast_typeops.mli | 6 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 13 | ||||
-rw-r--r-- | kernel/safe_typing.mli | 4 | ||||
-rw-r--r-- | kernel/term_typing.ml | 28 | ||||
-rw-r--r-- | kernel/term_typing.mli | 8 | ||||
-rw-r--r-- | library/declare.ml | 18 | ||||
-rw-r--r-- | library/declare.mli | 2 | ||||
-rw-r--r-- | library/global.ml | 4 | ||||
-rw-r--r-- | library/global.mli | 6 | ||||
-rw-r--r-- | toplevel/command.ml | 22 | ||||
-rw-r--r-- | toplevel/command.mli | 7 |
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 |