From 797736bbd7975926cc028a9f7c9c577e9c1e476b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 24 Nov 2017 11:02:02 +0100 Subject: 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. --- plugins/micromega/MExtraction.v | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) (limited to 'plugins') 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 *) -- cgit v1.2.3