diff options
| author | Hugo Herbelin | 2017-05-01 09:04:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-01 18:21:44 +0200 |
| commit | cea40f37ab638031b9d5c6434ee5651a16ea1f3e (patch) | |
| tree | 950c7d540bcd6fae24c0cd4262f8d0f086c1d6e6 /dev/include | |
| parent | 8511d1d9d903e419543e39eca83c64171da2663b (diff) | |
Fixing Set Rewriting Schemes bugs introduced in v8.5.
- Fixing a typo introduced in 31dbba5f.
- Adapting to computation of universe constraints in pretyping.
- Adding a regression test.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions