aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/engine.mllib
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-24 23:58:56 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-27 00:07:39 +0100
commit2206b405c19940ca4ded2179d371c21fd13f1b6b (patch)
treee6de3d347e53644439203cbfcb209a9fa4ffb462 /engine/engine.mllib
parent93db616a6cbebf37f2f4f983963a87a4f66972e7 (diff)
Adding a new folder corresponding to the low-level part of the pretyper
together with the tactic monad. The move is not complete yet, because some file candidates for this directory have almost useless dependencies in other ones that should not be moved.
Diffstat (limited to 'engine/engine.mllib')
-rw-r--r--engine/engine.mllib4
1 files changed, 4 insertions, 0 deletions
diff --git a/engine/engine.mllib b/engine/engine.mllib
new file mode 100644
index 000000000..4073f7e44
--- /dev/null
+++ b/engine/engine.mllib
@@ -0,0 +1,4 @@
+Logic_monad
+Termops
+Namegen
+Evd