diff options
author | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:50:59 +0000 |
---|---|---|
committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:50:59 +0000 |
commit | 1f48326c7edf7f6e7062633494d25b254a6db82c (patch) | |
tree | ad4abb42a890edb8a0f5c92bc658e0a26b365526 /tactics/tactics.ml | |
parent | 9ea680a275d3a93a35c3f09f53f26ee74d51fb00 (diff) |
Side effect free implementation of admit (Isabelle's oracle)
new Axiom in Logic.v, proof_admitted : False.
admit now simply cases proof_admitted and does
not create a new Axiom in the environment.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16673 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tactics.ml')
-rw-r--r-- | tactics/tactics.ml | 26 |
1 files changed, 1 insertions, 25 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ea8573052..06ad729d4 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3607,31 +3607,7 @@ let tclABSTRACT name_op tac gl = let admit_as_an_axiom gl = - let current_sign = Global.named_context() - and global_sign = pf_hyps gl in - let sign,secsign = - List.fold_right - (fun (id,_,_ as d) (s1,s2) -> - if mem_named_context id current_sign & - interpretable_as_section_decl (Context.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 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 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 - let gl = - exact_no_check - (applist (axiom, - List.rev (instance_from_named_context sign))) - gl in + let gl = simplest_case (Coqlib.build_coq_proof_admitted ()) gl in Pp.feedback Interface.AddedAxiom; gl |