diff options
| author | Maxime Dénès | 2017-06-13 01:05:14 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-13 01:05:14 +0200 |
| commit | 598ec175ea8ba6b424cc9ecf87f878494aef69a8 (patch) | |
| tree | d536c451975fcecc3ca6c704c075c2f03d03a9cc /plugins/micromega/MExtraction.v | |
| parent | 7e9a4aa4efa62d9fcded340c1c2f07a73021aca0 (diff) | |
| parent | f377960d80f5a31620b1105758b0c24aef828cd3 (diff) | |
Merge PR#772: 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 4d5c3b1d5b..2451aeada7 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. |