diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/Makefile | 7 | ||||
| -rw-r--r-- | test-suite/output-modulo-time/ltacprof_abstract.out | 15 | ||||
| -rw-r--r-- | test-suite/output/MExtraction.v | 12 |
3 files changed, 28 insertions, 6 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index dbd63a57b8..de669218ce 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -312,6 +312,13 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) rm $$tmpoutput; \ } > "$@" +# the expected output for the MExtraction test is +# /plugins/micromega/micromega.ml except with additional newline +output/MExtraction.out: ../plugins/micromega/micromega.ml + $(SHOW) GEN $@ + $(HIDE) cp $< $@ + $(HIDE) echo >> $@ + $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ diff --git a/test-suite/output-modulo-time/ltacprof_abstract.out b/test-suite/output-modulo-time/ltacprof_abstract.out index c60c5abddf..fef4fa248d 100644 --- a/test-suite/output-modulo-time/ltacprof_abstract.out +++ b/test-suite/output-modulo-time/ltacprof_abstract.out @@ -1,14 +1,17 @@ -total time: 0.964s +total time: 0.922s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─sleep' -------------------------------- 100.0% 100.0% 1 0.964s -─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.964s +─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.922s +─sleep' -------------------------------- 100.0% 100.0% 1 0.922s ─constructor --------------------------- 0.0% 0.0% 1 0.000s +─sleep --------------------------------- 0.0% 0.0% 0 0.000s tactic local total calls max ────────────────────────────────────────┴──────┴──────┴───────┴─────────┘ -─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.964s - ├─sleep' ------------------------------ 100.0% 100.0% 1 0.964s - └─constructor ------------------------- 0.0% 0.0% 1 0.000s +─abstract (sleep; constructor) --------- 0.0% 100.0% 1 0.922s + ├─sleep' ------------------------------ 100.0% 100.0% 1 0.922s + ├─constructor ------------------------- 0.0% 0.0% 1 0.000s + └─sleep ------------------------------- 0.0% 0.0% 0 0.000s + └sleep' ------------------------------ 0.0% 0.0% 0 0.000s 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. |