aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <enrico.tassi@inria.fr>2015-03-09 18:44:33 +0100
committerGravatar Enrico Tassi <enrico.tassi@inria.fr>2015-03-11 11:42:10 +0100
commitf36f1d07ee0b9b40d54b9fece942b00e8e5e5d50 (patch)
tree4b3d9cf2a0ed1ef4faa1d6bfccaaf0ca878a942d /theories/Init
parente4ad47fed594d6865f5bd29a159976cb072f0fae (diff)
admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)
- no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
Diffstat (limited to 'theories/Init')
-rw-r--r--theories/Init/Logic.v3
-rw-r--r--theories/Init/Prelude.v2
2 files changed, 1 insertions, 4 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index d2971552d..50f853f0e 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -22,9 +22,6 @@ 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.
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 4894eba4b..0efb8744d 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -23,4 +23,4 @@ Declare ML Module "cc_plugin".
Declare ML Module "ground_plugin".
Declare ML Module "recdef_plugin".
(* Default substrings not considered by queries like SearchAbout *)
-Add Search Blacklist "_admitted" "_subproof" "Private_".
+Add Search Blacklist "_subproof" "Private_".