| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-07-22 | Remove redundant data from VM case switch. | Pierre-Marie Pédrot | |
| No need to store the case_info, all the data is reconstructible from the context. Furthermore, this reconstruction is performed in a context where we already access the environment, so performance is not at stake. Hopefully this will also reduce the number of globally allocated VM values, since the switch representation now only depends on the shape of the inductive type. | |||
| 2020-07-01 | UIP in SProp | Gaëtan Gilbert | |
| 2019-03-14 | Documentation for SProp | Gaëtan Gilbert | |
| 2019-03-14 | Repair relevance marks in-kernel. | Gaëtan Gilbert | |
| Prevent errors when under annotating binders. | |||
| 2019-03-14 | Enable proof irrelevance for SProp. | Gaëtan Gilbert | |
| 2019-03-14 | Inductives in SProp, forbid primitive records with only sprop fields | Gaëtan Gilbert | |
| For nonsquashed: Either - 0 constructors - primitive record | |||
| 2019-03-14 | Add a non-cumulative impredicative universe SProp. | Gaëtan Gilbert | |
| Note currently it's impossible to define inductives in SProp because indtypes.ml and the pretyper aren't fully plugged. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |