diff options
| author | Gaëtan Gilbert | 2017-11-24 11:02:02 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-11-28 12:31:04 +0100 |
| commit | 797736bbd7975926cc028a9f7c9c577e9c1e476b (patch) | |
| tree | 551f4a6b277b0cb976b53032748ffec44d35c509 /test-suite/output | |
| parent | f303ed9fb26797b9ec7d172fe583e7ee607ae441 (diff) | |
Make the micromega extraction check a regular output test.
This allows us to enforce that it works without breaking the build
when it doesn't.
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/MExtraction.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v new file mode 100644 index 0000000000..352e422cf7 --- /dev/null +++ b/test-suite/output/MExtraction.v @@ -0,0 +1,12 @@ +Require Import micromega.MExtraction. +Require Import RingMicromega. +Require Import QArith. +Require Import VarMap. +Require Import ZMicromega. +Require Import QMicromega. +Require Import RMicromega. + +Recursive Extraction + List.map RingMicromega.simpl_cone (*map_cone indexes*) + denorm Qpower vm_add + n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. |