aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-08-08 18:50:59 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-08-08 18:50:59 +0000
commit1f48326c7edf7f6e7062633494d25b254a6db82c (patch)
treead4abb42a890edb8a0f5c92bc658e0a26b365526 /tactics/tactics.ml
parent9ea680a275d3a93a35c3f09f53f26ee74d51fb00 (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.ml26
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