diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/leminv.ml | 1 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 3 | ||||
| -rw-r--r-- | tactics/tactics.ml | 3 |
3 files changed, 5 insertions, 2 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index a6915461d7..1697c14654 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -235,6 +235,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op = declare_constant name (DefinitionEntry { const_entry_body = invProof; + const_entry_secctx = None; const_entry_type = None; const_entry_opaque = false }, IsProof Lemma) diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 805f4260a7..80930af42c 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1647,6 +1647,7 @@ let declare_projection n instance_id r = let typ = it_mkProd_or_LetIn typ ctx in let cst = { const_entry_body = term; + const_entry_secctx = None; const_entry_type = Some typ; const_entry_opaque = false } in @@ -1713,7 +1714,7 @@ let add_morphism_infer glob m n = let instance = build_morphism_signature m in if Lib.is_modtype () then let cst = Declare.declare_constant ~internal:Declare.KernelSilent instance_id - (Entries.ParameterEntry (instance,None), Decl_kinds.IsAssumption Decl_kinds.Logical) + (Entries.ParameterEntry (None,instance,None), Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance (Lazy.force proper_class) None glob (ConstRef cst)); declare_projection n instance_id (ConstRef cst) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 25a148bbdb..45eee91eef 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3516,7 +3516,8 @@ let admit_as_an_axiom gl = 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 (concl,None) in + 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 |