summaryrefslogtreecommitdiff
path: root/stm/lemmas.mli
diff options
context:
space:
mode:
Diffstat (limited to 'stm/lemmas.mli')
-rw-r--r--stm/lemmas.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index d0669d7a..a0ddd265 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -10,7 +10,6 @@ open Names
open Term
open Decl_kinds
open Constrexpr
-open Tacexpr
open Vernacexpr
open Pfedit