From b6733f0507e3e04fb6130b3f82a79e8835e1062f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 31 May 2017 00:30:00 +0200
Subject: Bump year in headers.

---
 interp/notation_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 5648821539..c46e5e9dac 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
-- 
cgit v1.2.3


From 849bf3600fe11fea876c9aeea69fe806b0c8c5d8 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Fri, 9 Jun 2017 12:30:42 -0400
Subject: Fix Bug #5568, no dup notation warnings on repeated module imports

---
 interp/notation_ops.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 5648821539..26e61d13af 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -47,9 +47,16 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
     | GHole _ | GSort _ | GLetIn _), _
       -> false
 
+(* helper for NVar, NVar case in eq_notation_constr *)
+let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None
+
 let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
 | NRef gr1, NRef gr2 -> eq_gr gr1 gr2
-| NVar id1, NVar id2 -> Int.equal (List.index Id.equal id1 vars1) (List.index Id.equal id2 vars2)
+| NVar id1, NVar id2 -> (
+   match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with
+   | Some n,Some m -> Int.equal n m
+   | None  ,None   -> Id.equal id1 id2
+   | _             -> false)
 | NApp (t1, a1), NApp (t2, a2) ->
   (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2
 | NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *)
-- 
cgit v1.2.3