diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 29 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
2 files changed, 31 insertions, 0 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5c0ed93575..198a17bcd9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1910,3 +1910,32 @@ let tclABSTRACT name_op tac gls = | None -> add_suffix (get_current_proof_name ()) "_subproof" in abstract_subproof s tac gls + + +let admit_as_an_axiom gls = + let env = Global.env() in + let current_sign = Global.named_context() + and global_sign = pf_hyps gls in + let sign,secsign = + List.fold_right + (fun (id,_,_ as d) (s1,s2) -> + if mem_named_context id current_sign & + interpretable_as_section_decl (Sign.lookup_named id current_sign) d + then (s1,add_named_decl d s2) + else (add_named_decl d s1,s2)) + global_sign (empty_named_context,empty_named_context) in + let name = add_suffix (get_current_proof_name ()) "_admitted" in + let na = next_global_ident_away false name (pf_ids_of_hyps gls) in + let concl = it_mkNamedProd_or_LetIn (pf_concl gls) sign in + if occur_existential concl then + if !Options.v7 then error "admit cannot handle existentials" + else error "\"admit\" cannot handle existentials"; + let axiom = + let cd = Entries.ParameterEntry concl in + let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in + constr_of_global (ConstRef con) + in + exact_no_check + (applist (axiom, + List.rev (Array.to_list (instance_from_named_context sign)))) + gls diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 34c4e6397b..5b03a79dd7 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -248,3 +248,5 @@ val generalize : constr list -> tactic val generalize_dep : constr -> tactic val tclABSTRACT : identifier option -> tactic -> tactic + +val admit_as_an_axiom : tactic |