aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofs.mllib
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-06 19:01:38 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-03-06 19:36:03 +0100
commit9e96794d6a4327761ce1ff992351199919431be1 (patch)
tree389b2b091c2d186490943c6db92c5eaa452bb5f4 /proofs/proofs.mllib
parent6ecbc9990a49a0dd51970c7fc8b13f39f02be773 (diff)
Moving Tactic_debug to tactics/ folder.
Diffstat (limited to 'proofs/proofs.mllib')
-rw-r--r--proofs/proofs.mllib1
1 files changed, 0 insertions, 1 deletions
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 47a637575..08556d62e 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -11,6 +11,5 @@ Redexpr
Refiner
Tacmach
Pfedit
-Tactic_debug
Clenv
Clenvtac