diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-07-08 14:43:57 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-07-08 14:43:57 +0200 |
| commit | e73d5db97cdb22cce2ee479469f62af3c4b6264a (patch) | |
| tree | 035d31018c2abec698eb49a205c60bbf5c24ba0d /lib/Camlcoq.ml | |
| parent | db2445b3b745abd1a26f5a832a29ca269c725277 (diff) | |
| download | compcert-kvx-e73d5db97cdb22cce2ee479469f62af3c4b6264a.tar.gz compcert-kvx-e73d5db97cdb22cce2ee479469f62af3c4b6264a.zip | |
Port to Coq 8.5pl2
Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
Diffstat (limited to 'lib/Camlcoq.ml')
| -rw-r--r-- | lib/Camlcoq.ml | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index 7e8a1018..5b5d37ee 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -56,8 +56,6 @@ module P = struct let one = Coq_xH let succ = Pos.succ let pred = Pos.pred - let add = Pos.add - let sub = Pos.sub let eq x y = (Pos.compare x y = Eq) let lt x y = (Pos.compare x y = Lt) let gt x y = (Pos.compare x y = Gt) @@ -106,8 +104,6 @@ module P = struct then Coq_xH else Coq_xI (of_int64 (Int64.shift_right_logical n 1)) - let (+) = add - let (-) = sub let (=) = eq let (<) = lt let (<=) = le @@ -124,11 +120,6 @@ module N = struct let zero = N0 let one = Npos Coq_xH - let succ = N.succ - let pred = N.pred - let add = N.add - let sub = N.sub - let mul = N.mul let eq x y = (N.compare x y = Eq) let lt x y = (N.compare x y = Lt) let gt x y = (N.compare x y = Gt) @@ -157,9 +148,6 @@ module N = struct let of_int64 n = if n = 0L then N0 else Npos (P.of_int64 n) - let (+) = add - let (-) = sub - let ( * ) = mul let (=) = eq let (<) = lt let (<=) = le |