diff options
| author | Pierre-Marie Pédrot | 2020-02-03 18:01:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-03 18:02:39 +0100 |
| commit | a4088339e1948e12f8c0a525577698bc67301a58 (patch) | |
| tree | 5a8421d07cfbcc535644a04f0ddac94330ca4c3a /pretyping/program.ml | |
| parent | 1c1c04d0e3e02ce461fb953f08e2d8c68e52ee63 (diff) | |
Test for #5617: Primitive projections confuse the termination checker.
Fixes #5617.
Diffstat (limited to 'pretyping/program.ml')
0 files changed, 0 insertions, 0 deletions