coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6743: Add notation {x & P} for sigT	Maxime Dénès	2018-03-08
\|\
* \|	Update headers following #6543.	Théo Zimmermann	2018-02-27
* \|	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-20
\| *	Add notation {x & P} for sigT	Tej Chajed	2018-02-12
\|/
*	A little reorganization of notations + a fix to #5608.	Hugo Herbelin	2017-08-29
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	plugins/ltac : avoid spurious .cmxs files	Pierre Letouzey	2017-06-15
*	Ltac as a plugin.	Pierre-Marie Pédrot	2017-02-17
*	Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...	Matthieu Sozeau	2016-04-04
\|\
* \|	Moving Eauto to a simple ML file.	Pierre-Marie Pédrot	2016-03-06
* \|	Moving the Tauto tactic to proper Ltac.	Pierre-Marie Pédrot	2016-02-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\ \
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \|	Removing auto from the tactic AST.	Pierre-Marie Pédrot	2015-12-24
\| \| *	Move type_scope into user space, fix some output logs	Jason Gross	2015-08-14
\| \| *	Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080	Jason Gross	2015-08-14
\| \|/ \|/\|
\| *	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-08-02
\|/
*	Fix various typos in documentation	Matěj Grabovský	2015-03-31
*	Update headers.	Maxime Dénès	2015-01-12
*	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-08-07
*	Moving argument-free tactics out of the AST into a dedicated	Pierre-Marie Pédrot	2014-05-16
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	Updating headers.	herbelin	2012-08-08
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	"A -> B" is a notation for "forall _ : A, B".	pboutill	2012-04-12
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Fixed extra space in printing notation { x & P } + minor other things	herbelin	2009-08-11
*	- Patch sur "intros until 0"	herbelin	2008-06-08
*	Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]	herbelin	2008-05-09
*	Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la	herbelin	2008-04-29
*	Gestion espaces dans notation _ = _ :> _	herbelin	2007-06-05
*	- Déplacement des types paramétriques prod, sum, option, identity,	herbelin	2006-05-28
*	Inutile de réserver les notations à base de '{ }'	herbelin	2004-12-06
*	Commentaires coqdoc	herbelin	2004-08-01
*	Nouvelle en-tête	herbelin	2004-07-16
*	Definition de la notation de la paire par un motif recursif	herbelin	2004-03-17
*	Décomposition automatique des règles d'analyse syntaxique pour les	herbelin	2004-02-12
*	Duplication temporaire des règles de syntaxe des paires	herbelin	2003-12-16
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
*	power associe a droite	marche	2003-12-05
*	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin	2003-11-29
*	Tri et typo	herbelin	2003-11-21
*	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...	barras	2003-11-13
*	%type au lieu de %T	herbelin	2003-11-12
*	petits changements de syntaxe	barras	2003-11-12
*	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entie...	herbelin	2003-11-01