diff options
Diffstat (limited to 'caml/Camlcoq.ml')
| -rw-r--r-- | caml/Camlcoq.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml index b0bb4ff9..fc5d2d87 100644 --- a/caml/Camlcoq.ml +++ b/caml/Camlcoq.ml @@ -7,6 +7,11 @@ open BinInt (* Integers *) +let rec camlint_of_nat n = + match n with + | O -> 0l + | S n -> Int32.add (camlint_of_nat n) 1l + let rec camlint_of_positive = function | Coq_xI p -> Int32.add (Int32.shift_left (camlint_of_positive p) 1) 1l | Coq_xO p -> Int32.shift_left (camlint_of_positive p) 1 |