diff options
| author |  Enrico Tassi <enrico.tassi@inria.fr> | 2015-03-09 18:44:33 +0100 |
|---|---|---|
| committer | Enrico Tassi <enrico.tassi@inria.fr> | 2015-03-11 11:42:10 +0100 |
| commit | f36f1d07ee0b9b40d54b9fece942b00e8e5e5d50 (patch) | |
| tree | 4b3d9cf2a0ed1ef4faa1d6bfccaaf0ca878a942d /test-suite/bugs/opened/HoTT_coq_120.v | |
| parent | e4ad47fed594d6865f5bd29a159976cb072f0fae (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/opened/HoTT_coq_120.v')
| -rw-r--r-- | test-suite/bugs/opened/HoTT_coq_120.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/HoTT_coq_120.v b/test-suite/bugs/opened/HoTT_coq_120.v index 7847c5e44..05ee6c7b6 100644 --- a/test-suite/bugs/opened/HoTT_coq_120.v +++ b/test-suite/bugs/opened/HoTT_coq_120.v @@ -1,3 +1,4 @@ +Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from 351 lines to 260 lines, then from 208 lines to 162 lines, then from 167 lines to 154 lines *) Set Universe Polymorphism. Generalizable All Variables. |