From d5cbd7b881dcc8b3599b3330e342f0aa55ef467f Mon Sep 17 00:00:00 2001 From: Nickolai Zeldovich Date: Fri, 8 Apr 2016 14:48:34 +0100 Subject: 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. --- plugins/extraction/ExtrOcamlZBigInt.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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". -- cgit v1.2.3