aboutsummaryrefslogtreecommitdiffstats
path: root/caml/Camlcoq.ml
diff options
context:
space:
mode:
authorxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-09-04 15:08:29 +0000
committerxleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2006-09-04 15:08:29 +0000
commit73729d23ac13275c0d28d23bc1b1f6056104e5d9 (patch)
treee3044ce75edb30377bd8c87356b7617eba5ed223 /caml/Camlcoq.ml
parentc79434827bf2bd71f857f4471f7bbf381fddd189 (diff)
downloadcompcert-73729d23ac13275c0d28d23bc1b1f6056104e5d9.tar.gz
compcert-73729d23ac13275c0d28d23bc1b1f6056104e5d9.zip
Fusion de la branche "traces":
- Ajout de traces d'evenements d'E/S dans les semantiques - Ajout constructions switch et allocation dynamique - Initialisation des variables globales - Portage Coq 8.1 beta Debut d'integration du front-end C: - Traduction Clight -> Csharpminor dans cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml/Camlcoq.ml')
-rw-r--r--caml/Camlcoq.ml5
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