From 59f2255105922f019be0905d188e638d49053e10 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
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 +
 1 file changed, 1 insertion(+)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index b4cf6e9430..3efd50b17f 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) ->
-- 
cgit v1.2.3