diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-10 12:59:44 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-10 13:01:24 +0200 |
| commit | af767e36829ada2b23f5d8eae631649e865392ae (patch) | |
| tree | fc850ddd224e3f6ed5acd6417d27bb71ff07dcbf /test-suite/success/primitiveproj.v | |
| parent | 6624459e492164b3d189e3518864379ff985bf8c (diff) | |
Parsing and printing of primitive projections, fix buggy behavior when
implicits do not allow to parse as an application and cleanup code.
Diffstat (limited to 'test-suite/success/primitiveproj.v')
| -rw-r--r-- | test-suite/success/primitiveproj.v | 14 |
1 files changed, 11 insertions, 3 deletions
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 02cb43db0..74083ac89 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -103,6 +103,14 @@ Set Printing All. Check p r. Unset Printing All. +Check p r (X:=nat). +Set Printing Projections. +Check p r (X:=nat). +Unset Printing Projections. +Set Printing All. +Check p r (X:=nat). +Unset Printing All. + (* Same elaboration, printing for p r *) (** Explicit version of the primitive projection, under applied w.r.t implicit arguments @@ -116,7 +124,7 @@ Check r.(@p). Unset Printing All. (** Explicit version of the primitive projection, applied to its implicit arguments - can be printed only using projection notation r.(p), r.(@p) in fully explicit form *) + can be printed using application notation r.(p), r.(@p) in fully explicit form *) Check r.(@p) nat. Set Printing Projections. Check r.(@p) nat. @@ -129,7 +137,7 @@ Parameter r' : R' nat. Check (r'.(p')). Set Printing Projections. -Check (r'.(p')). +Check (r'.(p')). Unset Printing Projections. Set Printing All. Check (r'.(p')). @@ -140,7 +148,7 @@ Unset Printing All. Of type forall X : Set, nat * X No Printing All: p' r' Set Printing Projections.: r'.(p') - Printing All: r'.(p') + Printing All: r'.(@p') *) Check p' r'. |