summaryrefslogtreecommitdiff
path: root/proofs/proofs.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proofs.mllib')
-rw-r--r--proofs/proofs.mllib9
1 files changed, 6 insertions, 3 deletions
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 05b86b1a..66001e77 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -1,12 +1,15 @@
+Goal
+Evar_refiner
+Proofview
+Proof
+Proof_global
Tacexpr
Proof_type
Redexpr
-Proof_trees
Logic
Refiner
-Evar_refiner
Tacmach
Pfedit
Tactic_debug
+Clenv
Clenvtac
-Decl_mode