aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/extend.mli
diff options
context:
space:
mode:
Diffstat (limited to 'intf/extend.mli')
-rw-r--r--intf/extend.mli4
1 files changed, 1 insertions, 3 deletions
diff --git a/intf/extend.mli b/intf/extend.mli
index 6b29fc747..3b14ceea9 100644
--- a/intf/extend.mli
+++ b/intf/extend.mli
@@ -6,14 +6,12 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Compat
-
(** Entry keys for constr notations *)
type side = Left | Right
type production_position =
- | BorderProd of side * gram_assoc option
+ | BorderProd of side * Compat.gram_assoc option
| InternalProd
type production_level =