diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/leminv.ml | 20 | ||||
| -rw-r--r-- | tactics/tactics.ml | 17 |
2 files changed, 19 insertions, 18 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 942cdc77e..c8a3ffd55 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -225,17 +225,15 @@ let inversion_scheme env sigma t sort dep_option inv_op = let add_inversion_lemma name env sigma t sort dep inv_op = let invProof = inversion_scheme env sigma t sort dep inv_op in - let _ = - declare_constant name - (DefinitionEntry - { const_entry_body = invProof; - const_entry_secctx = None; - const_entry_type = None; - const_entry_opaque = false; - const_entry_inline_code = false - }, - IsProof Lemma) - in () + let entry = { + const_entry_body = invProof; + const_entry_secctx = None; + const_entry_type = None; + const_entry_opaque = false; + const_entry_inline_code = false; + } in + let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in + () (* inv_op = Inv (derives de complete inv. lemma) * inv_op = InvNoThining (derives de semi inversion lemma) *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6ba5e0e04..a3733b3e7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3528,7 +3528,10 @@ let abstract_subproof id tac gl = let const = Pfedit.build_constant_by_tactic id secsign concl (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)) in let cd = Entries.DefinitionEntry const in - let lem = mkConst (Declare.declare_constant ~internal:Declare.KernelSilent id (cd,IsProof Lemma)) in + let decl = (cd, IsProof Lemma) in + (** ppedrot: seems legit to have abstracted subproofs as local*) + let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in + let lem = mkConst cst in exact_no_check (applist (lem,List.rev (Array.to_list (instance_from_named_context sign)))) gl @@ -3556,12 +3559,12 @@ let admit_as_an_axiom gl = let na = next_global_ident_away name (pf_ids_of_hyps gl) in let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in if occur_existential concl then error"\"admit\" cannot handle existentials."; - let axiom = - let cd = - Entries.ParameterEntry (Pfedit.get_used_variables(),concl,None) in - let con = Declare.declare_constant ~internal:Declare.KernelSilent na (cd,IsAssumption Logical) in - constr_of_global (ConstRef con) - in + let entry = (Pfedit.get_used_variables (), concl, None) in + let cd = Entries.ParameterEntry entry in + let decl = (cd, IsAssumption Logical) in + (** ppedrot: seems legit to have admitted subproofs as local*) + let con = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true na decl in + let axiom = constr_of_global (ConstRef con) in exact_no_check (applist (axiom, List.rev (Array.to_list (instance_from_named_context sign)))) |