aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/engine.mllib
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-04-13 16:31:01 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-04 13:47:12 +0200
commit5da0f107cb3332d5cd87fc352aef112f6b74fc97 (patch)
tree854d373e13b6ef39017e6bc2dd6d0c7e14a006cd /engine/engine.mllib
parenta6de02fcfde76f49b10d8481a2423692fa105756 (diff)
Moving Ftactic and Geninterp to the engine folder.
Diffstat (limited to 'engine/engine.mllib')
-rw-r--r--engine/engine.mllib2
1 files changed, 2 insertions, 0 deletions
diff --git a/engine/engine.mllib b/engine/engine.mllib
index 70b74edca..9ce5af819 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -7,3 +7,5 @@ Sigma
Proofview_monad
Evarutil
Proofview
+Ftactic
+Geninterp