diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-04 16:55:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-04-04 16:55:36 +0200 |
| commit | b7aa3064e50e34afe2e1a458f61e6e2b1f5d37f8 (patch) | |
| tree | 9198a8c2f4f1a62ac7e661365685fbb496950ada /test-suite/output | |
| parent | f95d33479cae45a5f6f18eb260e3c9ffcb605882 (diff) | |
| parent | 47abea3e05021450743756264c392ec5dc07b97c (diff) | |
Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Projections.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Projections.v | 11 |
2 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out new file mode 100644 index 000000000..e9c28faf1 --- /dev/null +++ b/test-suite/output/Projections.out @@ -0,0 +1,2 @@ +fun S : store => S.(store_funcs) + : store -> host_func diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v new file mode 100644 index 000000000..098a518dc --- /dev/null +++ b/test-suite/output/Projections.v @@ -0,0 +1,11 @@ + +Set Printing Projections. + +Class HostFunction := host_func : Type. + +Section store. + Context `{HostFunction}. + Record store := { store_funcs : host_func }. +End store. + +Check (fun (S:@store nat) => S.(store_funcs)). |