| Age | Commit message (Expand) | Author |
|---|
| 2020-04-21 | Moving the main Require Export Ltac in Prelude.v. | Hugo Herbelin |
| 2020-04-21 | Adding a Declare ML Module in empty file Ltac.v. | Hugo Herbelin |
| 2020-03-30 | new sig notations and spaces added | Olivier Laurent |
| 2020-03-18 | Update headers in the whole code base. | Théo Zimmermann |
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann |
| 2018-09-10 | Adapting standard library to the introduction of "Declare Scope". | Hugo Herbelin |
| 2018-03-08 | Merge PR #6743: Add notation {x & P} for sigT | Maxime Dénès |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann |
| 2018-02-20 | Trying a hack to support {'pat|P} without breaking compatibility. | Hugo Herbelin |
| 2018-02-20 | User-level support for Gonthier-Ssreflect's "if t then pat then u else v". | Hugo Herbelin |
| 2018-02-12 | Add notation {x & P} for sigT | Tej Chajed |
| 2017-08-29 | A little reorganization of notations + a fix to #5608. | Hugo Herbelin |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot |
| 2017-06-15 | plugins/ltac : avoid spurious .cmxs files | Pierre Letouzey |
| 2017-02-17 | Ltac as a plugin. | Pierre-Marie Pédrot |
| 2016-04-04 | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into... | Matthieu Sozeau |
| 2016-03-06 | Moving Eauto to a simple ML file. | Pierre-Marie Pédrot |
| 2016-02-22 | Moving the Tauto tactic to proper Ltac. | Pierre-Marie Pédrot |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-12-24 | Removing auto from the tactic AST. | Pierre-Marie Pédrot |
| 2015-08-14 | Move type_scope into user space, fix some output logs | Jason Gross |
| 2015-08-14 | Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080 | Jason Gross |
| 2015-08-02 | Reverting 16 last commits, committed mistakenly using the wrong push command. | Hugo Herbelin |
| 2015-08-02 | Adding a notation { x & P } for { x : _ & P }. | Hugo Herbelin |
| 2015-03-31 | Fix various typos in documentation | Matěj Grabovský |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-08-07 | Instead of relying on a trick to make the constructor tactic parse, put | Pierre-Marie Pédrot |
| 2014-08-07 | Removing the "constructor" tactic from the AST. | Pierre-Marie Pédrot |
| 2014-05-16 | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot |
| 2014-05-12 | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-05 | ZArith + other : favor the use of modern names instead of compat notations | letouzey |
| 2012-04-12 | "A -> B" is a notation for "forall _ : A, B". | pboutill |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2009-08-11 | Fixed extra space in printing notation { x & P } + minor other things | herbelin |
| 2008-06-08 | - Patch sur "intros until 0" | herbelin |
| 2008-05-09 | Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ] | herbelin |
| 2008-04-29 | Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la | herbelin |
| 2007-06-05 | Gestion espaces dans notation _ = _ :> _ | herbelin |
| 2006-05-28 | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin |
| 2004-12-06 | Inutile de réserver les notations à base de '{ }' | herbelin |
| 2004-08-01 | Commentaires coqdoc | herbelin |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2004-03-17 | Definition de la notation de la paire par un motif recursif | herbelin |
| 2004-02-12 | Décomposition automatique des règles d'analyse syntaxique pour les | herbelin |
| 2003-12-16 | Duplication temporaire des règles de syntaxe des paires | herbelin |
| 2003-12-15 | modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes | barras |
| 2003-12-05 | power associe a droite | marche |
