Notations can now accept dummy arguments. If ever a bound variable is not

used, they are automatically flagged as only parsing. CAVEAT: unused
arguments are not typechecked, because they are dropped before the
interpretation phase.

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;
+}