summaryrefslogtreecommitdiff
path: root/tactics/tactics.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tactics.mllib')
-rw-r--r--tactics/tactics.mllib12
1 files changed, 3 insertions, 9 deletions
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 2c5edc20..09330260 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,5 +1,3 @@
-Ftactic
-Geninterp
Dnet
Dn
Btermdn
@@ -14,15 +12,11 @@ Equality
Contradiction
Inv
Leminv
-Tacsubst
-Taccoerce
-Tacenv
Hints
Auto
-Tacintern
+Eauto
+Class_tactics
Tactic_matching
-Tacinterp
-Evar_tactics
Term_dnet
+Eqdecide
Autorewrite
-Tactic_option