diff options
| author | Hugo Herbelin | 2016-07-18 22:41:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-07-19 11:20:59 +0200 |
| commit | 692e33acd9a44d5c00fe515bd9b87728d2c872a7 (patch) | |
| tree | c6cb3e3afc2630568378c622bf5f9bde7fe4c963 /interp/notation_ops.ml | |
| parent | 63f3ca8973a877f22db4d5fea541c1fab1b706f2 (diff) | |
Notations: fixing multiple binders used as terms in reverse order.
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 8 |
1 files changed, 6 insertions, 2 deletions
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 |