From ca67a3fb4184c81449101d9a0cec511ccde09d43 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 22 Dec 2013 01:02:21 +0100
Subject: 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.

---
 intf/notation_term.mli | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'intf/notation_term.mli')

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;
+}
-- 
cgit v1.2.3