summaryrefslogtreecommitdiff
path: root/ltac/ltac.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'ltac/ltac.mllib')
-rw-r--r--ltac/ltac.mllib22
1 files changed, 0 insertions, 22 deletions
diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib
deleted file mode 100644
index fc51e48a..00000000
--- a/ltac/ltac.mllib
+++ /dev/null
@@ -1,22 +0,0 @@
-Taccoerce
-Tacsubst
-Tacenv
-Tactic_debug
-Tacintern
-Tacentries
-Profile_ltac
-Tacinterp
-Evar_tactics
-Tactic_option
-Extraargs
-G_obligations
-Coretactics
-Extratactics
-Profile_ltac_tactics
-G_auto
-G_class
-Rewrite
-G_rewrite
-Tauto
-G_eqdecide
-G_ltac