aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.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 /tactics/tactics.mllib
parenta6de02fcfde76f49b10d8481a2423692fa105756 (diff)
Moving Ftactic and Geninterp to the engine folder.
Diffstat (limited to 'tactics/tactics.mllib')
-rw-r--r--tactics/tactics.mllib2
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index ab8069225..48722f655 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,5 +1,3 @@
-Ftactic
-Geninterp
Dnet
Dn
Btermdn