From b16ae82270be36e6578b36737d57a3792ae25f71 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 28 Oct 2019 18:26:22 +0100
Subject: ppvernac: bidi hints use & not |

---
 vernac/ppvernac.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 5cffc39839..3dbf7afb78 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1082,7 +1082,7 @@ let string_of_definition_object_kind = let open Decls in function
               let rec print_arguments n nbidi l =
                 match n, nbidi, l with
                   | Some 0, _, l -> spc () ++ str"/" ++ print_arguments None nbidi l
-                  | _, Some 0, l -> spc () ++ str"|" ++ print_arguments n None l
+                  | _, Some 0, l -> spc () ++ str"&" ++ print_arguments n None l
                   | None, None, [] -> mt()
                   | _, _, [] ->
                     let dummy = {name=Anonymous; recarg_like=false;
-- 
cgit v1.2.3