Merge PR #965: Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.

8 files changed, 29 insertions, 29 deletions

diff --git a/API/API.ml b/API/API.ml
index c952e123d..1d7a4a4f4 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -43,7 +43,7 @@ module Cbytecodes = Cbytecodes
 (* module Copcodes *)
 module Cemitcodes = Cemitcodes
 (* module Nativevalues *)
-(* module Primitives *)
+(* module CPrimitives *)
 module Opaqueproof = Opaqueproof
 module Declareops = Declareops
 module Retroknowledge = Retroknowledge
diff --git a/kernel/primitives.ml b/kernel/cPrimitives.ml
index 14c11bf10..14c11bf10 100644
--- a/kernel/primitives.ml
+++ b/kernel/cPrimitives.ml
diff --git a/kernel/primitives.mli b/kernel/cPrimitives.mli
index 8cdffb670..8cdffb670 100644
--- a/kernel/primitives.mli
+++ b/kernel/cPrimitives.mli
diff --git a/kernel/environ.ml b/kernel/environ.ml
index d2c737ab0..621a9931d 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -624,39 +624,39 @@ fun rk value field ->
           native_constant_dynamic = Some Nativelambda.compile_dynamic_int31;
         }
     | KInt31 (_, Int31Plus) -> int31_binop_from_const Cbytecodes.Kaddint31
-							  Primitives.Int31add
+							  CPrimitives.Int31add
     | KInt31 (_, Int31PlusC) -> int31_binop_from_const Cbytecodes.Kaddcint31
-							   Primitives.Int31addc
+							   CPrimitives.Int31addc
     | KInt31 (_, Int31PlusCarryC) -> int31_binop_from_const Cbytecodes.Kaddcarrycint31
-								Primitives.Int31addcarryc
+								CPrimitives.Int31addcarryc
     | KInt31 (_, Int31Minus) -> int31_binop_from_const Cbytecodes.Ksubint31
-							   Primitives.Int31sub
+							   CPrimitives.Int31sub
     | KInt31 (_, Int31MinusC) -> int31_binop_from_const Cbytecodes.Ksubcint31
-							    Primitives.Int31subc
+							    CPrimitives.Int31subc
     | KInt31 (_, Int31MinusCarryC) -> int31_binop_from_const
-	                                Cbytecodes.Ksubcarrycint31 Primitives.Int31subcarryc
+	                                Cbytecodes.Ksubcarrycint31 CPrimitives.Int31subcarryc
     | KInt31 (_, Int31Times) -> int31_binop_from_const Cbytecodes.Kmulint31
-							   Primitives.Int31mul
+							   CPrimitives.Int31mul
     | KInt31 (_, Int31TimesC) -> int31_binop_from_const Cbytecodes.Kmulcint31
-							   Primitives.Int31mulc
+							   CPrimitives.Int31mulc
     | KInt31 (_, Int31Div21) -> int31_op_from_const 3 Cbytecodes.Kdiv21int31
-                                                           Primitives.Int31div21
+                                                           CPrimitives.Int31div21
     | KInt31 (_, Int31Diveucl) -> int31_binop_from_const Cbytecodes.Kdivint31
-							 Primitives.Int31diveucl
+							 CPrimitives.Int31diveucl
     | KInt31 (_, Int31AddMulDiv) -> int31_op_from_const 3 Cbytecodes.Kaddmuldivint31
-                                                         Primitives.Int31addmuldiv
+                                                         CPrimitives.Int31addmuldiv
     | KInt31 (_, Int31Compare) -> int31_binop_from_const Cbytecodes.Kcompareint31
-							     Primitives.Int31compare
+							     CPrimitives.Int31compare
     | KInt31 (_, Int31Head0) -> int31_unop_from_const Cbytecodes.Khead0int31
-							  Primitives.Int31head0
+							  CPrimitives.Int31head0
     | KInt31 (_, Int31Tail0) -> int31_unop_from_const Cbytecodes.Ktail0int31
-							  Primitives.Int31tail0
+							  CPrimitives.Int31tail0
     | KInt31 (_, Int31Lor) -> int31_binop_from_const Cbytecodes.Klorint31
-							 Primitives.Int31lor
+							 CPrimitives.Int31lor
     | KInt31 (_, Int31Land) -> int31_binop_from_const Cbytecodes.Klandint31
-							  Primitives.Int31land
+							  CPrimitives.Int31land
     | KInt31 (_, Int31Lxor) -> int31_binop_from_const Cbytecodes.Klxorint31
-							  Primitives.Int31lxor
+							  CPrimitives.Int31lxor
     | _ -> empty_reactive_info
 
 let _ = Hook.set Retroknowledge.dispatch_hook dispatch
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 994634854..917e4f6f1 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -17,7 +17,7 @@ Opaqueproof
 Declarations
 Entries
 Nativevalues
-Primitives
+CPrimitives
 Declareops
 Retroknowledge
 Conv_oracle
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index da7fcd6f2..e08d913bc 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -296,7 +296,7 @@ type primitive =
   | MLmagic
   | MLarrayget
   | Mk_empty_instance
-  | Coq_primitive of Primitives.t * (prefix * constant) option
+  | Coq_primitive of CPrimitives.t * (prefix * constant) option
 
 let eq_primitive p1 p2 =
   match p1, p2 with
@@ -361,9 +361,9 @@ let primitive_hash = function
   | MLsub -> 33
   | MLmul -> 34
   | MLmagic -> 35
-  | Coq_primitive (prim, None) -> combinesmall 36 (Primitives.hash prim)
+  | Coq_primitive (prim, None) -> combinesmall 36 (CPrimitives.hash prim)
   | Coq_primitive (prim, Some (prefix,kn)) ->
-     combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (Primitives.hash prim))
+     combinesmall 37 (combine3 (String.hash prefix) (Constant.hash kn) (CPrimitives.hash prim))
   | Mk_proj -> 38
   | MLarrayget -> 39
   | Mk_empty_instance -> 40
@@ -921,7 +921,7 @@ let merge_branches t =
 
 
 type prim_aux = 
-  | PAprim of string * constant * Primitives.t * prim_aux array
+  | PAprim of string * constant * CPrimitives.t * prim_aux array
   | PAml of mllambda
 
 let add_check cond args =
@@ -988,11 +988,11 @@ let compile_prim decl cond paux =
         | Int31lt -> 
            if Sys.word_size = 64 then
              app_prim Mk_bool [|(app_prim MLlt (args_to_int args))|]
-           else app_prim (Coq_primitive (Primitives.Int31lt,None)) args
+           else app_prim (Coq_primitive (CPrimitives.Int31lt,None)) args
         | Int31le ->
            if Sys.word_size = 64 then
              app_prim Mk_bool [|(app_prim MLle (args_to_int args))|]
-           else app_prim (Coq_primitive (Primitives.Int31le, None)) args
+           else app_prim (Coq_primitive (CPrimitives.Int31le, None)) args
 	| Int31lsl  -> of_int (mk_lsl (args_to_int args))
 	| Int31lsr  -> of_int (mk_lsr (args_to_int args))
 	| Int31land -> of_int (mk_land (args_to_int args))
@@ -1752,9 +1752,9 @@ let pp_mllam fmt l =
     | MLarrayget -> Format.fprintf fmt "Array.get"
     | Mk_empty_instance -> Format.fprintf fmt "Univ.Instance.empty"
     | Coq_primitive (op,None) ->
-       Format.fprintf fmt "no_check_%s" (Primitives.to_string op)
+       Format.fprintf fmt "no_check_%s" (CPrimitives.to_string op)
     | Coq_primitive (op, Some (prefix,kn)) ->
-        Format.fprintf fmt "%s %a" (Primitives.to_string op)
+        Format.fprintf fmt "%s %a" (CPrimitives.to_string op)
 		       pp_mllam (MLglobal (Gconstant (prefix, kn)))
   in
   Format.fprintf fmt "@[%a@]" pp_mllam l
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index cb79877e8..2353470f0 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -30,7 +30,7 @@ and lambda =
   | Lapp          of lambda * lambda array
   | Lconst        of prefix * pconstant
   | Lproj         of prefix * constant (* prefix, projection name *)
-  | Lprim         of prefix * constant * Primitives.t * lambda array
+  | Lprim         of prefix * constant * CPrimitives.t * lambda array
   | Lcase         of annot_sw * lambda * lambda * lam_branches 
                   (* annotations, term being matched, accu, branches *)
   | Lif           of lambda * lambda * lambda
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index bfa3bf941..156e4f834 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -38,5 +38,5 @@ val compile_dynamic_int31 : bool -> prefix -> constructor -> lambda array ->
 val before_match_int31 : inductive -> bool -> prefix -> constructor -> lambda ->
 			 lambda
 
-val compile_prim : Primitives.t -> constant -> bool -> prefix -> lambda array ->
+val compile_prim : CPrimitives.t -> constant -> bool -> prefix -> lambda array ->
 		   lambda