1 files changed, 6 insertions, 0 deletions
diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index 411b14f1f1..ac5e0f5f9c 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -73,3 +73,9 @@ type notation_var_internalization_type =
 type interpretation =
     (Id.t * (subscopes * notation_var_instance_type)) list *
     notation_constr
+
+type notation_interp_env = {
+  ninterp_var_type : notation_var_internalization_type Id.Map.t;
+  ninterp_rec_vars : Id.t Id.Map.t;
+  mutable ninterp_only_parse : bool;
+}