diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-24 11:02:02 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-28 12:31:04 +0100 |
| commit | 797736bbd7975926cc028a9f7c9c577e9c1e476b (patch) | |
| tree | 551f4a6b277b0cb976b53032748ffec44d35c509 /plugins/micromega | |
| 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 '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 *) |