{"push_id":2337480815,"size":1,"distinct_size":1,"ref":"refs/heads/univ-cumul","head":"2fdddac45dc6879a224685c51e34ad0fa417861a","before":"e2e2e6835c3658ded788d9be5e409e15219441f3","commits":[{"sha":"2fdddac45dc6879a224685c51e34ad0fa417861a","author":{"name":"Gaëtan Gilbert","email":"5bbfdd0af0dfb2940814c6b5e8e839007e186364@skyskimmer.net"},"message":"Allow using cumulativity without forcing strict constraints.\n\nPreviously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative\ninductive would try to generate a constraint [i = j] and use\ncumulativity only if this resulted in an inconsistency. This is\nconfusingly different from the behaviour with [Type] and means\ncumulativity can only be used to lift between universes related by\nstrict inequalities. (This isn't a kernel restriction so there might\nbe some workaround to send the kernel the right constraints, but\nnot in a nice way.)\n\nSee modified test for more details of what is now possible.\n\nTechnical notes:\n\nWhen universe constraints were inferred by comparing the shape of\nterms without reduction, cumulativity was not used and so too-strict\nequality constraints were generated. Then in order to use cumulativity\nwe had to make this comparison fail to fall back to full conversion.\n\nWhen unifiying 2 instances of a cumulative inductive type, if there\nare any Irrelevant universes we try to unify them if they are\nflexible.","distinct":true,"url":"https://api.github.com/repos/SkySkimmer/coq/commits/2fdddac45dc6879a224685c51e34ad0fa417861a"}]}
{"actor":{"display_login":"SkySkimmer"}}