diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-12 17:42:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-12 19:18:55 +0200 |
| commit | 07335670c4339f9c4ae620088d9352be67a77714 (patch) | |
| tree | d95d3828877e4e9676e16c0cf186fe805aff4eea /kernel/nativecode.ml | |
| parent | 83e506e9a4b8140320e8f505b9ef6e4da05d710c (diff) | |
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.
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 16 |
1 files changed, 8 insertions, 8 deletions
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 |