| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Simpl less (so that cbn will not simpl too much) |  Pierre Boutillier | 2014-10-01 |
| | | |||
| * | Now parsing rules of ML-declared tactics are only made available after the |  Pierre-Marie Pédrot | 2014-05-12 |
| | | | | | | | | | | | | | | corresponding Declare ML Module command. This changes essentially two things: 1. ML plugins are forced to use the DECLARE PLUGIN statement before any TACTIC EXTEND statement. The plugin name must be exactly the string passed to the Declare ML Module command. 2. ML tactics are only made available after the Coq module that does the corresponding Declare ML Module is imported. This may break a few things, as it already broke quite some uses of omega in the stdlib. | ||
| * | Replace nat indices with positive one in Btauto. |  ppedrot | 2012-06-28 |
| | | | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15499 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
| * | Added a Btauto plugin, that solves boolean tautologies. | ppedrot | 2012-01-13 |
| git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14897 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |