| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2008-04-26 | Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour | herbelin |
| 2008-04-25 | Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve | herbelin |
| 2008-04-15 | * added a subsection to explain the automatic declaration of schemes: | vsiles |
| 2008-04-15 | - Un peu de doc, préparation du CHANGES pour la release. | herbelin |
| 2008-04-15 | typo | vsiles |
| 2008-04-13 | Bugs, nettoyage, et améliorations diverses | herbelin |
| 2008-03-10 | Indexation de pose proof, et par la même occasion du nouveau specialize | herbelin |
| 2008-03-07 | f_equal, revert, specialize in ML, contradict in better Ltac (+doc) | letouzey |
| 2008-03-06 | repair for commit 10612 (due to grammar order, some syntaxes weren't working) | letouzey |
| 2008-03-01 | Rework on rich forms of rewrite | letouzey |
| 2008-02-03 | Add new files theories/Program/Basics.v and theories/Classes/Relations.v | msozeau |
| 2008-01-31 | Debug implementation of dependent induction/dependent destruction and documen... | msozeau |
| 2008-01-05 | Standardisation du format des références croisées vers Figure, Section, Ch... | herbelin |
| 2007-10-16 | Added the doc for the new Scheme Equality command | vsiles |
| 2007-09-19 | Indication de quel type de constantes est dépliable dans "simpl" (cf | herbelin |
| 2007-07-09 | More natural notation for intro pattern: @a -> ?a | glondu |
| 2007-07-06 | Adding a syntax for "n-ary" rewrite: | letouzey |
| 2007-07-06 | extension of the rename tactic: the following is now allowed: | letouzey |
