aboutsummaryrefslogtreecommitdiff
path: root/API
diff options
context:
space:
mode:
authorHugo Herbelin2017-05-01 09:04:17 +0200
committerHugo Herbelin2017-05-01 18:21:44 +0200
commitcea40f37ab638031b9d5c6434ee5651a16ea1f3e (patch)
tree950c7d540bcd6fae24c0cd4262f8d0f086c1d6e6 /API
parent8511d1d9d903e419543e39eca83c64171da2663b (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 'API')
0 files changed, 0 insertions, 0 deletions