aboutsummaryrefslogtreecommitdiff
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/lemmas.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index e2ddf79df8..93f24b42cb 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -9,8 +9,6 @@
open Names
open Term
open Decl_kinds
-open Constrexpr
-open Vernacexpr
open Pfedit
type 'a declaration_hook