From 59f2255105922f019be0905d188e638d49053e10 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 24 Jun 2016 14:18:50 +0200
Subject: Fixing #4854 (regression introduced in 4d25b224 in relation with
 #4592).

---
 interp/notation_ops.ml           | 1 +
 test-suite/output/Notations2.out | 4 ++++
 test-suite/output/Notations2.v   | 5 +++++
 3 files changed, 10 insertions(+)

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index b4cf6e943..3efd50b17 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -750,6 +750,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
 
   (* Matching notation variable *)
   | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 r1
+  | GVar (_,id1), NVar id2 when is_onlybinding_meta id2 metas -> snd (bind_binding_env alp sigma id2 (Name id1))
 
   (* Matching recursive notations for terms *)
   | r1, NList (x,_,iter,termin,lassoc) ->
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 6ff1d3837..d9ce42c60 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -54,3 +54,7 @@ end
      : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0}
 exist (Q x) y conj
      : {x0 : A | Q x x0}
+% i
+     : nat -> nat
+% j
+     : nat -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 4e0d135d7..3cf89818d 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -106,3 +106,8 @@ Check fun x (H:le x 0) => exist (le x) 0 H.
 
 Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y).
 Check (exist (Q x) y conj).
+
+(* Check bug #4854 *)
+Notation "% i" := (fun i : nat => i) (at level 0, i ident).
+Check %i.
+Check %j.
-- 
cgit v1.2.3