aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-03-20 03:37:55 +0100
committerPierre-Marie Pédrot2016-03-20 21:26:40 +0100
commit6de9f13ba666250ea397c7db1d9d37075a9dc1c2 (patch)
tree54907ef7210dceaa788720484bbd833fc0546a1a /dev
parentf39543a752d05e5661749bbc3f221d75e525b3b4 (diff)
Moving Tacenv to Hightactics.
Diffstat (limited to 'dev')
-rw-r--r--dev/printers.mllib1
1 files changed, 0 insertions, 1 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index aad56f586b..9f25ba55e7 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -200,7 +200,6 @@ Ppdecl_proof
Egramml
Egramcoq
Tacsubst
-Tacenv
Trie
Dn
Btermdn