Remove custom extraction of comparison to int in ExtrOCamlInt63

coq · Dec 6, 2021 · cce9a7f · cce9a7f
1 parent 9284726
commit cce9a7f
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 3 deletions.
diff --git a/doc/changelog/10-standard-library/15294-extract-comparison.rst b/doc/changelog/10-standard-library/15294-extract-comparison.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+  `ExtrOCamlInt63` no longer extracts `comparison` to `int` in OCaml;
+  the extraction of `Uint63.compare` and `Sint63.compare` was also adapted accordingly
+  (`#15294 <https://github.com/coq/coq/pull/15294>`_,
+  fixes `#15280 <https://github.com/coq/coq/issues/15280>`_,
+  by Li-yao Xia).
diff --git a/theories/extraction/ExtrOCamlInt63.v b/theories/extraction/ExtrOCamlInt63.v
@@ -16,7 +16,6 @@ From Coq Require Uint63 Sint63 Extraction.
 
 Extract Inductive bool => bool [ true false ].
 Extract Inductive prod => "( * )" [ "" ].
-Extract Inductive comparison => int [ "0" "(-1)" "1" ].
 Extract Inductive DoubleType.carry => "Uint63.carry" [ "Uint63.C0" "Uint63.C1" ].
 
 (** Primitive types and operators. *)
@@ -56,8 +55,8 @@ Extract Constant Uint63.diveucl => "Uint63.diveucl".
 Extract Constant Uint63.diveucl_21 => "Uint63.div21".
 Extract Constant Uint63.addmuldiv => "Uint63.addmuldiv".
 
-Extract Constant Uint63.compare => "Uint63.compare".
-Extract Constant Sint63.compare => "Uint63.compares".
+Extract Constant Uint63.compare => "(fun x y -> let c = Uint63.compare x y in if c = 0 then Eq else if c < 0 then Lt else Gt)".
+Extract Constant Sint63.compare => "(fun x y -> let c = Uint63.compares x y in if c = 0 then Eq else if c < 0 then Lt else Gt)".
 
 Extract Constant Uint63.head0 => "Uint63.head0".
 Extract Constant Uint63.tail0 => "Uint63.tail0".