| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2003-11-29 | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin |
| 2003-11-21 | Tri et typo | herbelin |
| 2003-11-13 | moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc... | barras |
| 2003-11-12 | %type au lieu de %T | herbelin |
| 2003-11-12 | petits changements de syntaxe | barras |
| 2003-11-01 | Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie... | herbelin |
| 2003-10-30 | Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ... | herbelin |
| 2003-10-28 | Ajout %core; MAJ niveau connecteurs logique | herbelin |
| 2003-10-22 | reorganisation des niveaux (ex: = est a 70) | barras |
| 2003-10-16 | nouvelle syntaxe de ltac | barras |
| 2003-10-13 | Enregistrement '^' en v8 | herbelin |
| 2003-09-21 | Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi... | herbelin |
| 2003-08-10 | Affichage {}+{}, niveau paire au plus haut | herbelin |
| 2003-06-10 | Deplacement delimiteur T dans Notations | herbelin |
| 2003-05-29 | Bug niveau | herbelin |
