From dfadb394640b3d09eb6134b73d0f3e931bd70af1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 28 Sep 2016 15:29:58 +0200
Subject: Warning about similar notations now up to alpha-conversion.

This allows to define on purpose the very same notation in different
files, as currently the notations for *, +, - in Nat.v and Peano.v
(with the first one using variables n and m and the second one using
the default variables used by Infix, namely x and y).

This makes also the "notation-overridden" warning less enigmatic
facing two notations which are the same up to the choice of names.
---
 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 854e222e30..4ebd3ddd80 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -12,7 +12,7 @@ open Glob_term
 
 (** {5 Utilities about [notation_constr]} *)
 
-val eq_notation_constr : notation_constr -> notation_constr -> bool
+val eq_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool
 
 (** Substitution of kernel names in interpretation data                *)
 
-- 
cgit v1.2.3