Fixing interpretation of notations w/ opposite instances of a recursive pattern.

3 files changed, 29 insertions, 3 deletions

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ef363f540..80c09745d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -237,6 +237,8 @@ let check_is_hole id = function GHole _ -> () | t ->
     strbrk "In recursive notation with binders, " ++ pr_id id ++
     strbrk " is expected to come without type.")
 
+let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'
+
 let compare_recursive_parts found f (iterator,subc) =
   let diff = ref None in
   let terminator = ref None in
@@ -284,7 +286,13 @@ let compare_recursive_parts found f (iterator,subc) =
 	user_err_loc (subtract_loc loc1 loc2,"",
           str "Both ends of the recursive pattern are the same.")
     | Some (x,y,Some lassoc) ->
-        let newfound = (pi1 !found, (x,y) :: pi2 !found, pi3 !found) in
+        let newfound,x,y,lassoc =
+          if List.mem_f (pair_equal Id.equal Id.equal) (x,y) (pi2 !found) then
+            !found,x,y,lassoc
+          else if List.mem_f (pair_equal Id.equal Id.equal) (y,x) (pi2 !found) then
+            !found,y,x,not lassoc
+          else
+            (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in
 	let iterator =
 	  f (if lassoc then subst_glob_vars [y,GVar(Loc.ghost,x)] iterator
 	  else iterator) in
@@ -357,8 +365,6 @@ let notation_constr_and_vars_of_glob_constr a =
   (* Side effect *)
   t, !found
 
-let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b'
-
 let check_variables nenv (found,foundrec,foundrecbinding) =
   let recvars = nenv.ninterp_rec_vars in
   let fold _ y accu = Id.Set.add y accu in
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index b3d2580ac..823418cc1 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -6,3 +6,14 @@
      : nat * nat * (nat * nat)
 pair (pair O (S (S O))) (pair (S (S O)) O)
      : prod (prod nat nat) (prod nat nat)
+<< 0, 2, 4 >>
+     : nat * nat * nat * (nat * (nat * nat))
+<< 0, 2, 4 >>
+     : nat * nat * nat * (nat * (nat * nat))
+(0, 2, 4, (2, (2, 0)))
+     : nat * nat * nat * (nat * (nat * nat))
+(0, 2, 4, (0, (2, 4)))
+     : nat * nat * nat * (nat * (nat * nat))
+pair (pair (pair O (S (S O))) (S (S (S (S O)))))
+  (pair (S (S (S (S O)))) (pair (S (S O)) O))
+     : prod (prod (prod nat nat) nat) (prod nat (prod nat nat))
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 32d70ac18..f37772534 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -10,3 +10,12 @@ Check ((0,2),(2,2)).
 Unset Printing Notations.
 Check [<0,2>].
 Set Printing Notations.
+
+Notation "<< x , y , .. , z >>" := ((.. (x,y) .., z),(z, .. (y,x) ..)).
+Check <<0,2,4>>.
+Check (((0,2),4),(4,(2,0))).
+Check (((0,2),4),(2,(2,0))).
+Check (((0,2),4),(0,(2,4))).
+Unset Printing Notations.
+Check <<0,2,4>>.
+Set Printing Notations.