diff options
| author |  Matej Košík <matej.kosik@inria.fr> | 2017-06-12 19:28:52 +0200 |
|---|---|---|
| committer | Matej Košík <matej.kosik@inria.fr> | 2017-06-12 19:33:22 +0200 |
| commit | f377960d80f5a31620b1105758b0c24aef828cd3 (patch) | |
| tree | 2bb842c6645e62686f110e02912e8bcded6b5d2f /plugins/micromega/MExtraction.v | |
| parent | 83d8b081c02cfde83c8fd93102f8f1aae3fe87b3 (diff) | |
Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to generate them later.
Diffstat (limited to 'plugins/micromega/MExtraction.v')
| -rw-r--r-- | plugins/micromega/MExtraction.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v index 4d5c3b1d5..2451aeada 100644 --- a/plugins/micromega/MExtraction.v +++ b/plugins/micromega/MExtraction.v @@ -48,7 +48,7 @@ Extract Constant Rmult => "( * )". Extract Constant Ropp => "fun x -> - x". Extract Constant Rinv => "fun x -> 1 / x". -Extraction "plugins/micromega/micromega.ml" +Extraction "plugins/micromega/generated_micromega.ml" List.map simpl_cone (*map_cone indexes*) denorm Qpower vm_add n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find. |