From bc3b07f639f04295bc440f42d5aa2420c07ecee6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 14 Aug 2017 01:18:23 +0200
Subject: Fixing a typo in printing notations with recursive binders.

Was causing a failure to print recursive binders used twice or more in
the same notation.
---
 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 99e18f09ef..f605729217 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -824,7 +824,7 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
        alp, b :: bl
     | _ -> raise No_match in
     let alp, bl = unify alp bl bl' in
-    let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in
+    let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in
     alp, add_bindinglist_env sigma var bl
   with Not_found ->
     alp, add_bindinglist_env sigma var bl
-- 
cgit v1.2.3