diff options
| -rw-r--r-- | interp/notation.ml | 12 | ||||
| -rw-r--r-- | test-suite/output/Notations3.out | 17 | ||||
| -rw-r--r-- | test-suite/output/bug_9180.out | 3 | ||||
| -rw-r--r-- | test-suite/output/locate.out | 5 |
4 files changed, 16 insertions, 21 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 04856a30f2..d57c4f3abf 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1986,7 +1986,7 @@ let pr_scope_classes sc = spc() ++ prlist_with_sep spc pr_scope_class l) let pr_notation_info prglob ntn c = - str "\"" ++ str ntn ++ str "\" := " ++ + str "\"" ++ str ntn ++ str "\" :=" ++ brk (1,2) ++ prglob (Notation_ops.glob_constr_of_notation_constr c) let pr_notation_status on_parsing on_printing = @@ -2007,7 +2007,7 @@ let pr_non_empty spc pp = if pp = mt () then mt () else spc ++ pp let pr_notation_data prglob (on_parsing,on_printing,{ not_interp = (_, r); not_location = (_, df) }) = - hov 0 (pr_notation_info prglob df r ++ pr_non_empty (spc ()) (pr_notation_status on_parsing on_printing)) + hov 0 (pr_notation_info prglob df r ++ pr_non_empty (brk(1,2)) (pr_notation_status on_parsing on_printing)) let extract_notation_data (main,extra) = let main = match main with @@ -2174,18 +2174,18 @@ let locate_notation prglob ntn scope = match ntns with | [] -> str "Unknown notation" | _ -> - str "Notation" ++ fnl () ++ prlist_with_sep fnl (fun (ntn,l) -> let scope = find_default ntn scopes in prlist_with_sep fnl (fun (sc,(on_parsing,on_printing,{ not_interp = (_, r); not_location = (_, df) })) -> hov 0 ( + str "Notation" ++ brk (1,2) ++ pr_notation_info prglob df r ++ (if String.equal sc default_scope then mt () - else (spc () ++ str ": " ++ str sc)) ++ + else (brk (1,2) ++ str ": " ++ str sc)) ++ (if Option.equal String.equal (Some sc) scope - then spc () ++ str "(default interpretation)" else mt ()) ++ - pr_non_empty (spc ()) (pr_notation_status on_parsing on_printing))) + then brk (1,2) ++ str "(default interpretation)" else mt ()) ++ + pr_non_empty (brk (1,2)) (pr_notation_status on_parsing on_printing))) l) ntns let collect_notation_in_scope scope sc known = diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index abada44da7..bd22d45059 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -231,16 +231,13 @@ fun l : list nat => match l with : list nat -> list nat Arguments foo _%list_scope -Notation -"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope -(default interpretation) -"'exists' ! x .. y , p" := ex - (unique - (fun x => .. (ex (unique (fun y => p))) ..)) -: type_scope (default interpretation) -Notation -"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope -(default interpretation) +Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) + : type_scope (default interpretation) +Notation "'exists' ! x .. y , p" := + (ex (unique (fun x => .. (ex (unique (fun y => p))) ..))) : type_scope + (default interpretation) +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope + (default interpretation) 1 subgoal ============================ diff --git a/test-suite/output/bug_9180.out b/test-suite/output/bug_9180.out index ed4892b389..f035d0252a 100644 --- a/test-suite/output/bug_9180.out +++ b/test-suite/output/bug_9180.out @@ -1,4 +1,3 @@ -Notation -"n .+1" := S n : nat_scope (default interpretation) +Notation "n .+1" := (S n) : nat_scope (default interpretation) forall x : nat, x.+1 = x.+1 : Prop diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out index 473db2d312..93d9d6cf7b 100644 --- a/test-suite/output/locate.out +++ b/test-suite/output/locate.out @@ -1,3 +1,2 @@ -Notation -"b1 && b2" := if b1 then b2 else false (default interpretation) -"x && y" := andb x y : bool_scope +Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation) +Notation "x && y" := (andb x y) : bool_scope |