From 07335670c4339f9c4ae620088d9352be67a77714 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Aug 2017 17:42:09 +0200 Subject: Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml. Indeed OCaml has a similar file and this conflicts, at least in debugger. --- kernel/nativecode.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'kernel/nativecode.ml') 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 -- cgit v1.2.3