From 9e8c57419b473fdb3f9fbb8251d1843ec0e6f884 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
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.
---
 interp/notation_ops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation_ops.mli')

diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 4ebd3ddd8..c8fcbf741 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -29,7 +29,7 @@ val ldots_var : Id.t
     bound by the notation; also interpret recursive patterns           *)
 
 val notation_constr_of_glob_constr : notation_interp_env ->
-  glob_constr -> notation_constr
+  glob_constr -> notation_constr * reversibility_flag
 
 (** Re-interpret a notation as a [glob_constr], taking care of binders *)
 
-- 
cgit v1.2.3