aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proofs.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proofs.mllib')
-rw-r--r--proofs/proofs.mllib2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 66001e77a..6b8fbf24b 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -3,7 +3,7 @@ Evar_refiner
Proofview
Proof
Proof_global
-Tacexpr
+Tacops
Proof_type
Redexpr
Logic