| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-10-09 | No bidirectionality when expected type for lambda is an evar. | Gaëtan Gilbert | |
| This fixes #12623 (bidirectionality breaks impredicativity). | |||
| 2019-01-10 | Remove Printing Primitive Projection Compatibility | Gaëtan Gilbert | |
| The code to generate the legacy bodies is moved to its only user in extraction. It almost seems like we could remove it (ie no special extraction code for primitive projection constants) but then we run into issues with automatic unboxing eg `Record foo := { a : nat; b : a <= 5 }.` gets extracted to `type foo = nat` and (if we remove the special code) `let a = a`. | |||
| 2018-10-10 | [test-suite] rename a file | Vincent Laporte | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |