aboutsummaryrefslogtreecommitdiff
path: root/src/tac2expr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/tac2expr.mli')
-rw-r--r--src/tac2expr.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index c787870c65..e57b0ba3ef 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Loc
-open Genarg
open Names
open Libnames