diff options
| author | Hugo Herbelin | 2020-09-04 19:04:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-10-10 23:19:32 +0200 |
| commit | 4c090da84c1cf2c4e37b9ddd5b2321c474f19e60 (patch) | |
| tree | 5076c75a07712b3120b6e3831681fb56b382b990 /test-suite | |
| parent | 5ef7598009bf49feafd632c0171a1bb14bef6448 (diff) | |
New spacing/formatting in Locate Notation, Print Scopes, Print Visibility.
Diffstat (limited to 'test-suite')
| -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 |
3 files changed, 10 insertions, 15 deletions
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 |