| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Force polymorphic definitions to have no internal constraints. |  Pierre-Marie Pédrot | 2018-01-11 |
| | | | | | | | | The main contender was the abstract tactic that was generating useless constraints for polymorphic subproofs that happened to contain themselves monomorphic subproofs. We had to fix the test-suite for one particular corner-case instance that looked more like a bug than anything else. | ||
| * | Getting rid of abstraction breaking code in tclABSTRACT. | Pierre-Marie Pédrot | 2017-07-14 |
| This is probably the hardest case of them all, because tclABSTRACT fundamentally relies on the names of universes from the constant instance being the same as the one in the current goal. Adding to that the fact that the kernel is doing strange things when provided with a polymorphic definition with body universe constraints, it turns out to be a hellish nightmare to handle properly. At some point we need to clarifiy this in the kernel as well, although we leave it for some other patch. | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |