From b663b735adaf546192ff5b25b608dda55e05f3d8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 19 Jul 2016 10:44:31 +0200
Subject: Notations with multiple recursive binders: fixing use of
 alpha-conversion.

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

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 8045213459..1b84ccff48 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -779,8 +779,8 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
     match bl, bl' with
     | [], [] -> alp, []
     | b :: bl, b' :: bl' ->
-       let alp,bl = unify alp bl bl' in
        let alp,b = unify_binder alp b b' in
+       let alp,bl = unify alp bl bl' in
        alp, b :: bl
     | _ -> raise No_match in
     let alp, bl = unify alp bl bl' in
-- 
cgit v1.2.3