aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3329.v
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 /test-suite/bugs/closed/3329.v
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 'test-suite/bugs/closed/3329.v')
-rw-r--r--test-suite/bugs/closed/3329.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3329.v b/test-suite/bugs/closed/3329.v
index f7e368f8f..ecb09e843 100644
--- a/test-suite/bugs/closed/3329.v
+++ b/test-suite/bugs/closed/3329.v
@@ -1,3 +1,4 @@
+Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from original input, then from 12095 lines to 869 lines, then from 792 lines to 504 lines, then from 487 lines to 353 lines, then from 258 lines to 174 lines, then from 164 lines to 132 lines, then from 129 lines to 99 lines *)
Set Universe Polymorphism.
Generalizable All Variables.