diff options
| author | Vincent Laporte | 2019-04-01 19:40:53 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-04-01 19:40:53 +0000 |
| commit | 424c1973e96dfbf3b2e3245d735853ffa9600373 (patch) | |
| tree | af087fa873c709e0066c8f6d81898f3aeae59b21 /test-suite/output | |
| parent | 943fdd3277909f5229d95eb2e486944b0258648c (diff) | |
| parent | 6f1634d2f822037a482436a64d3ef3bfb2fac2a0 (diff) | |
Merge PR #9725: Lia: various impovements (support for #8764, fix #9268 and #9615)
Reviewed-by: Zimmi48
Ack-by: fajb
Reviewed-by: vbgl
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/MExtraction.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v index 36992e4dda..7429a521b3 100644 --- a/test-suite/output/MExtraction.v +++ b/test-suite/output/MExtraction.v @@ -7,6 +7,8 @@ Require Import QMicromega. Require Import RMicromega. Recursive Extraction - List.map simpl_cone (*map_cone indexes*) - denorm Qpower vm_add + Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula + ZMicromega.cnfZ ZMicromega.bound_problem_fr QMicromega.cnfQ + List.map simpl_cone (*map_cone indexes*) + denorm Qpower vm_add normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. |