| Age | Commit message (Expand) | Author |
|---|---|---|
| 2014-03-11 | vi2vo: universes handling finally fixed | Enrico Tassi |
| 2014-02-26 | checker and votour ported to new vo format (after -vi2vo) | Enrico Tassi |
| 2013-09-14 | Slightly more compact representation of 'a substituted type, | ppedrot |
| 2013-08-22 | Change in vo format : digest aren't Marshalled anymore | letouzey |
| 2013-08-20 | Declarations.mli: reorganization of modular structures | letouzey |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-04-15 | 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 |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |