diff options
| -rw-r--r-- | interp/coqlib.ml | 2 | ||||
| -rw-r--r-- | interp/coqlib.mli | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 26 | ||||
| -rw-r--r-- | theories/Init/Logic.v | 3 |
4 files changed, 7 insertions, 25 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 3a041a27f..9ce330078 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -338,6 +338,7 @@ let build_coq_inversion_eq_true_data () = (* The False proposition *) let coq_False = lazy_init_constant ["Logic"] "False" +let coq_proof_admitted = lazy_init_constant ["Logic"] "proof_admitted" (* The True proposition and its unique proof *) let coq_True = lazy_init_constant ["Logic"] "True" @@ -359,6 +360,7 @@ let build_coq_True () = Lazy.force coq_True let build_coq_I () = Lazy.force coq_I let build_coq_False () = Lazy.force coq_False +let build_coq_proof_admitted () = Lazy.force coq_proof_admitted let build_coq_not () = Lazy.force coq_not let build_coq_and () = Lazy.force coq_and let build_coq_conj () = Lazy.force coq_conj diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 5fb206bec..d9c0d3ae0 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -150,6 +150,7 @@ val build_coq_sumbool : constr delayed (** Connectives The False proposition *) val build_coq_False : constr delayed +val build_coq_proof_admitted : constr delayed (** The True proposition and its unique proof *) val build_coq_True : constr delayed 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 diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 804784b30..9251d00ff 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -21,6 +21,9 @@ Inductive True : Prop := (** [False] is the always false proposition *) Inductive False : Prop :=. +(** [proof_admitted] is used to implement the admit tactic *) +Axiom proof_admitted : False. + (** [not A], written [~A], is the negation of [A] *) Definition not (A:Prop) := A -> False. |