From 7c044bd9b5bca4970f6a936d5b6d5484bcb79397 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 24 Mar 2015 16:01:03 +0100
Subject: Fixing equality of notation_constrs. Fixes bug #4136.

---
 interp/notation_ops.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'interp/notation_ops.mli')

diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 7283ed6f12..c6770deea2 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -25,6 +25,8 @@ val ldots_var : Id.t
 (** FIXME: nothing to do here *)
 val eq_glob_constr : glob_constr -> glob_constr -> bool
 
+val eq_notation_constr : notation_constr -> notation_constr -> bool
+
 (** Re-interpret a notation as a [glob_constr], taking care of binders     *)
 
 val glob_constr_of_notation_constr_with_binders : Loc.t ->
-- 
cgit v1.2.3