Merge PR#747: Fix Bug #5568, no dup notation warnings on repeated module imports

1 files changed, 8 insertions, 1 deletions

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? *)