| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Slightly more compact representation of 'a substituted type, |  ppedrot | 2013-09-14 |
| * | Change in vo format : digest aren't Marshalled anymore |  letouzey | 2013-08-22 |
| * | Declarations.mli: reorganization of modular structures | letouzey | 2013-08-20 |
| * | State Transaction Machine |  gareuselesinge | 2013-08-08 |
| * | Checker: vo validation checks the absence of Var/Evar/Meta | letouzey | 2013-04-15 |
| * | Checker: vo validation is now done in check.ml (and always) | letouzey | 2013-04-15 |
| * | Checker: empty sections hardcoded in cb and mind | letouzey | 2013-04-15 |
| * | Checker: reified encoding of .vo types in values.ml | letouzey | 2013-04-15 |
| * | Checker: regroup all vo-related types in cic.mli | letouzey | 2013-04-15 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |