| Age | Commit message (Expand) | Author |
|---|
| 2011-10-07 | A new tactic is_var to check whether a term is a goal/section variable | letouzey |
| 2011-09-26 | Added support for referring to subterms of the goal by pattern. | herbelin |
| 2011-09-23 | auto with nocore : disable the use of the core database (wish #2188) | letouzey |
| 2011-09-02 | Bug 2589: Documentation patch of Hendrik Tews | pboutill |
| 2011-09-01 | Several bug reports came from confusions between generalize and set. | pboutill |
| 2010-12-24 | Precision in documentation of "decide equality" | glondu |
| 2010-12-23 | Remove the two-argument variant of "decide equality" | glondu |
| 2010-12-23 | More precise documentation for instantiate | glondu |
| 2010-12-02 | Documentation for tactic constr_eq | glondu |
| 2010-12-02 | Add tactic has_evar (#2433) | glondu |
| 2010-12-02 | Add tactic is_evar (Closes: #2433) | glondu |
| 2010-11-03 | Fix typo in "Hint Extern" doc | glondu |
| 2010-07-27 | Minor fixes: | msozeau |
| 2010-06-18 | Documentation of clear dependent and revert dependent | letouzey |
| 2010-06-08 | Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction". | herbelin |
| 2010-06-07 | Backporting part of r12970 to trunk (deprecation of double induction). | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-27 | small detail about Scheme Equality | vsiles |
| 2010-02-26 | Correction du bug #2214 + maj liens web | notin |
| 2010-01-30 | Update CHANGES, add documentation for new commands/tactics and do a bit | msozeau |
| 2009-11-08 | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin |
| 2009-11-03 | Report de la révision #12208 de la v8.2 (correction du bug #2126) | notin |
| 2009-10-08 | Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False' | letouzey |
| 2009-09-13 | - Inductive types in the "using" option of auto/eauto/firstorder are | herbelin |
| 2009-09-10 | Added syntax "exists bindings, ..., bindings" for iterated "exists". | herbelin |
| 2009-06-22 | Report de la révision #12200 (bug #2125) | notin |
| 2009-06-06 | Applying Ian Lynagh's documentation fixes patch (see bug #2112) | herbelin |
| 2009-05-09 | - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence | herbelin |
| 2009-03-20 | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ... | letouzey |
| 2009-01-13 | - Standardized prefix use of "Local"/"Global" modifiers as decided in | herbelin |
| 2009-01-03 | Fixed two problems: | herbelin |
| 2008-12-29 | - Added support for subterm matching in SearchAbout. | herbelin |
| 2008-12-09 | About "apply in": | herbelin |
| 2008-10-27 | - Fixed many "Theorem with" bugs. | herbelin |
| 2008-10-24 | Fix doc of apply in (see coq-club message 26 September 2008) | herbelin |
| 2008-10-19 | - Export de pattern_ident vers les ARGUMENT EXTEND and co. | herbelin |
| 2008-10-11 | Backporting 11445 from 8.2 to trunk (negative conditions in | herbelin |
| 2008-09-14 | Add user syntax for creating hint databases [Create HintDb foo | msozeau |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-06-29 | Lissage de la gestion des chemins de chargement de fichiers : | herbelin |
| 2008-06-21 | - Implantation de la suggestion 1873 sur discriminate. Au final, | herbelin |
| 2008-06-10 | - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs) | herbelin |
| 2008-06-09 | Fix a typo | glondu |
| 2008-06-09 | Documentation de "instantiate". | glondu |
| 2008-06-09 | - Documentation de admit et Print Assumptions. | herbelin |
| 2008-06-08 | - Extension de "generalize" en "generalize c as id at occs". | herbelin |
| 2008-06-01 | Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in | letouzey |
| 2008-06-01 | remove additional occurrences of +/- forgotten in commit 11030 | letouzey |
| 2008-06-01 | Bactrack sur +, - dans rewrite qui, redondants avec ->, <-, n'en sont qu'à | herbelin |
| 2008-05-12 | - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to | msozeau |
