diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-20 00:31:47 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-20 00:31:47 +0100 |
| commit | 547ec33c0742206a2820171636634abc2070c405 (patch) | |
| tree | 5732d6e30243d9cc6c50c89dc0aacc3408263970 /plugins/micromega | |
| parent | f431dac2e219cb2a76b22e452d6e407869d89f42 (diff) | |
| parent | 797736bbd7975926cc028a9f7c9c577e9c1e476b (diff) | |
Merge PR #6234: Make the micromega extraction check a regular output test.
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/MExtraction.v | 17 |
1 files changed, 7 insertions, 10 deletions
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index e5b5854f0..362cc3a59 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -49,16 +49,13 @@ Extract Constant Rmult => "( * )". Extract Constant Ropp => "fun x -> - x". Extract Constant Rinv => "fun x -> 1 / x". -(** We now extract to stdout, see comment in Makefile.build *) - -(*Extraction "plugins/micromega/micromega.ml" *) -Recursive Extraction - List.map simpl_cone (*map_cone indexes*) - denorm Qpower vm_add - n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. - - - +(** In order to avoid annoying build dependencies the actual + extraction is only performed as a test in the test suite. *) +(* Extraction "plugins/micromega/micromega.ml" *) +(* Recursive Extraction *) +(* List.map simpl_cone (*map_cone indexes*) *) +(* denorm Qpower vm_add *) +(* n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. *) (* Local Variables: *) (* coding: utf-8 *) |