aboutsummaryrefslogtreecommitdiff
path: root/src/tac2env.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/tac2env.mli')
-rw-r--r--src/tac2env.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/tac2env.mli b/src/tac2env.mli
index b82923765d..022c518143 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -10,7 +10,6 @@ open Genarg
open Names
open Libnames
open Nametab
-open Tac2dyn
open Tac2expr
open Tac2ffi