diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-25 12:49:12 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-25 12:49:12 +0200 |
| commit | 2f75922ad52e334b7bcc3a26c2ecb1602c85fc2f (patch) | |
| tree | 3ba950c021df581a004a4af158880558eb2dbe14 /plugins/micromega | |
| parent | 03e4f9c3da333d13553b4ea3247b0c36c124995e (diff) | |
| parent | cb316573aa1d09433531e7c67e320c14ef05c3e2 (diff) | |
Merge PR#481: [option] Remove support for non-synchronous options.
Diffstat (limited to 'plugins/micromega')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index b6ad784d9..053bb6fa1 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -65,7 +65,6 @@ let _ = let int_opt l vref = { - optsync = true; optdepr = false; optname = List.fold_right (^) l ""; optkey = l ; @@ -75,7 +74,6 @@ let _ = let lia_enum_opt = { - optsync = true; optdepr = false; optname = "Lia Enum"; optkey = ["Lia";"Enum"]; |