aboutsummaryrefslogtreecommitdiff
path: root/API
diff options
context:
space:
mode:
authorMaxime Dénès2017-08-18 22:14:59 +0200
committerMaxime Dénès2017-08-18 22:14:59 +0200
commit325890a83a2b073d9654b5615c585cd65a376fbd (patch)
treee8df2e678ae250675d9c1f1dca48647d598e1a38 /API
parent809cf4676c75d9a00f1fcd47e3c7d871a3dec83e (diff)
parent07335670c4339f9c4ae620088d9352be67a77714 (diff)
Merge PR #965: Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.
Diffstat (limited to 'API')
-rw-r--r--API/API.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/API/API.ml b/API/API.ml
index c952e123d4..1d7a4a4f46 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