diff options
| author | JPR | 2019-05-23 23:28:55 +0200 |
|---|---|---|
| committer | JPR | 2019-05-23 23:28:55 +0200 |
| commit | d306f5428db0d034aea55d3f0699c67c1f296cc1 (patch) | |
| tree | 540bcc09ec46c8a360cda9ed7fafa9ab631d3716 /test-suite/output | |
| parent | 5cfdc20560392c2125dbcee31cfd308d5346b428 (diff) | |
Fixing typos - Part 3
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Notations3.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index dcc8bd7165..29614c032a 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -209,7 +209,7 @@ Notation "'exists_mixed' x .. y , P" := (ex (fun x => forall z:nat, .. (ex (fun Check exists_mixed x y '(u,t), x+y=0/\u+t=0. Check exists_mixed x y '(z,t), x+y=0/\z+t=0. -(* Check that intermediary let-in are inserted inbetween instances of +(* Check that intermediary let-in are inserted in between instances of the repeated pattern *) Notation "'exists_true' x .. y , P" := (exists x, True /\ .. (exists y, True /\ P) ..) (at level 200, x binder). Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0. |