Skip to content
Snippets Groups Projects
Commit 1cd87015 authored by xleroy's avatar xleroy
Browse files

MAJ extraction after changes in Integers

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
parent 8d40eb31
No related branches found
No related tags found
No related merge requests found
......@@ -18,7 +18,7 @@ let more_likely (c: condexpr) (ifso: stmt) (ifnot: stmt) = false
module IntOrd =
struct
type t = Integers.int
type t = Integers.Int.int
let compare x y =
if Integers.Int.eq x y then 0 else
if Integers.Int.ltu x y then -1 else 1
......
......@@ -15,6 +15,7 @@
open Datatypes
open BinPos
open BinInt
open Integers
(* Integers *)
......@@ -28,7 +29,7 @@ let camlint_of_z = function
| Zpos p -> camlint_of_positive p
| Zneg p -> Int32.neg (camlint_of_positive p)
let camlint_of_coqint : Integers.int -> int32 = camlint_of_z
let camlint_of_coqint : Int.int -> int32 = camlint_of_z
let rec camlint_of_nat = function
| O -> 0
......@@ -50,7 +51,7 @@ let z_of_camlint n =
if n > 0l then Zpos (positive_of_camlint n)
else Zneg (positive_of_camlint (Int32.neg n))
let coqint_of_camlint (n: int32) : Integers.int =
let coqint_of_camlint (n: int32) : Int.int =
(* Interpret n as unsigned so that resulting Z is in range *)
if n = 0l then Z0 else Zpos (positive_of_camlint n)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment