aboutsummaryrefslogtreecommitdiff
path: root/kernel/kernel.mllib
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 /kernel/kernel.mllib
parent809cf4676c75d9a00f1fcd47e3c7d871a3dec83e (diff)
parent07335670c4339f9c4ae620088d9352be67a77714 (diff)
Merge PR #965: Moving file primitive.ml to cPrimitive.ml to avoid conflict with OCaml.
Diffstat (limited to 'kernel/kernel.mllib')
-rw-r--r--kernel/kernel.mllib2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 9946348541..917e4f6f14 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -17,7 +17,7 @@ Opaqueproof
Declarations
Entries
Nativevalues
-Primitives
+CPrimitives
Declareops
Retroknowledge
Conv_oracle