diff options
| author | Hugo Herbelin | 2020-11-03 02:11:33 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-04 17:33:43 +0100 |
| commit | 091bfff6ce37a303550e79abb23fdc992a28f7e3 (patch) | |
| tree | 1c58695f2aa1d658fde2ff09a90c267cb0e2dc9a /test-suite | |
| parent | 7f90e6e0aa8dd27c64bac0dbc4b247ebb33d4aca (diff) | |
Fixes #13298: primitive projections needs a correct typing environment.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/Search_bug13298.out | 1 | ||||
| -rw-r--r-- | test-suite/output/Search_bug13298.v | 3 |
2 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/output/Search_bug13298.out b/test-suite/output/Search_bug13298.out new file mode 100644 index 0000000000..18488c790f --- /dev/null +++ b/test-suite/output/Search_bug13298.out @@ -0,0 +1 @@ +snd: forall c : c, fst c = 0 diff --git a/test-suite/output/Search_bug13298.v b/test-suite/output/Search_bug13298.v new file mode 100644 index 0000000000..9a75321c64 --- /dev/null +++ b/test-suite/output/Search_bug13298.v @@ -0,0 +1,3 @@ +Set Primitive Projections. +Record c : Type := { fst : nat; snd : fst = 0 }. +Search concl:fst. |