diff options
| author |  Nickolai Zeldovich <nickolai@csail.mit.edu> | 2016-04-08 14:48:34 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2016-04-09 00:45:45 +0200 |
| commit | d5cbd7b881dcc8b3599b3330e342f0aa55ef467f (patch) | |
| tree | 9a616287bf8e4be55a1b46f690506504c281bb7d | |
| parent | 84f079fa31723b6a97edc50ca7a81e1eb19e759c (diff) | |
Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.v
The extraction of [Z] into Ocaml's [Big_int] passed arguments in the
wrong order to [Big.compare_case] for [Pos.compare_cont]. It seems
unlikely this ever worked before.
| -rw-r--r-- | plugins/extraction/ExtrOcamlZBigInt.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v index 9a1a4aa01..c9e8eac0c 100644 --- a/plugins/extraction/ExtrOcamlZBigInt.v +++ b/plugins/extraction/ExtrOcamlZBigInt.v @@ -46,7 +46,7 @@ Extract Constant Pos.max => "Big.max". Extract Constant Pos.compare => "fun x y -> Big.compare_case Eq Lt Gt x y". Extract Constant Pos.compare_cont => - "fun x y c -> Big.compare_case c Lt Gt x y". + "fun c x y -> Big.compare_case c Lt Gt x y". Extract Constant N.add => "Big.add". Extract Constant N.succ => "Big.succ". |