summaryrefslogtreecommitdiff
path: root/proofs/proofs.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proofs.mllib')
-rw-r--r--proofs/proofs.mllib10
1 files changed, 7 insertions, 3 deletions
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 66001e77..32bf5576 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -1,12 +1,16 @@
+Miscprint
Goal
Evar_refiner
+Proof_using
+Proof_type
+Proof_errors
+Logic_monad
+Proofview_monad
+Logic
Proofview
Proof
Proof_global
-Tacexpr
-Proof_type
Redexpr
-Logic
Refiner
Tacmach
Pfedit