| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-09-26 | Implement section discharging inside kernel. | Pierre-Marie Pédrot | |
| This patch is minimalistic, insofar as it is only untying the dependency loop between Declare and Safe_typing. Nonetheless, it is already quite big, thus we will polish it afterwards. | |||
| 2019-09-25 | Move the Lib section data into the kernel. | Pierre-Marie Pédrot | |
| Due to the redundancy with some other declaration-specific data from the kernel, we also seize the opportunity to clean it up. Note also that discharging is still performed outside of the kernel for now. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |