From f36f1d07ee0b9b40d54b9fece942b00e8e5e5d50 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 9 Mar 2015 18:44:33 +0100
Subject: 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
---
 interp/coqlib.ml  | 2 --
 interp/coqlib.mli | 1 -
 2 files changed, 3 deletions(-)

(limited to 'interp')

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index e722615a9b..02504c9202 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -349,7 +349,6 @@ 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"
@@ -371,7 +370,6 @@ 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 986a4385c1..41204a715b 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -160,7 +160,6 @@ 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
-- 
cgit v1.2.3