From 9e8c57419b473fdb3f9fbb8251d1843ec0e6f884 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 4 Oct 2016 13:27:29 +0200
Subject: Quick fix to #4595 (making notations containing "ltac:" unused for
 printing).

Also getting rid of a global side-effect.
---
 intf/notation_term.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'intf/notation_term.mli')

diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index 883b017727..1ab9980a5c 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -73,10 +73,11 @@ type interpretation =
     (Id.t * (subscopes * notation_var_instance_type)) list *
     notation_constr
 
+type reversibility_flag = bool
+
 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;
 }
 
 type grammar_constr_prod_item =
-- 
cgit v1.2.3