From 692e33acd9a44d5c00fe515bd9b87728d2c872a7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 18 Jul 2016 22:41:31 +0200
Subject: Notations: fixing multiple binders used as terms in reverse order.

---
 interp/notation_ops.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index e6b5dc50b5..8045213459 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -287,9 +287,13 @@ let compare_recursive_parts found f f' (iterator,subc) =
           str "Both ends of the recursive pattern are the same.")
     | Some (x,y,Some lassoc) ->
         let newfound,x,y,lassoc =
-          if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) then
+          if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) ||
+             List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi3 !found)
+          then
             !found,x,y,lassoc
-          else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) then
+          else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) ||
+                  List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi3 !found)
+          then
             !found,y,x,not lassoc
           else
             (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in
-- 
cgit v1.2.3