| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2013-03-12 | Updated Exninfo to the new Store type. | ppedrot | |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16268 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
| 2013-02-18 | Adding more primitives to Exninfo | ppedrot | |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16214 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
| 2013-02-18 | Added exception enrichment. Now one can define additional arbitrary | ppedrot | |
| information worn by exceptions. The implementation is quite hackish but it should work nonetheless. Basically, it adds an additional cell to exceptions arguments, in which you can put whatever you want. By typing invariants, you may not reach this cell by normal means, so it should be safe. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16212 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |