coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Allowing to extend the Print Grammar command generically.	Pierre-Marie Pédrot	2016-09-14
*	Unplugging Tacexpr in several interface files.	Pierre-Marie Pédrot	2016-09-08
*	Moving the tactic related code from Metasyntax to a new file.	Pierre-Marie Pédrot	2016-03-20
*	Infering atomic ML entries from their grammar.	Pierre-Marie Pédrot	2016-02-01
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Indexing existentially quantified entries returned by interp_entry_name.	Pierre-Marie Pédrot	2015-10-27
\|/
*	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg	2015-06-26
*	Update headers.	Maxime Dénès	2015-01-12
*	Notation: option to attach extra pretty printing rules to notations	Enrico Tassi	2014-09-29
*	Qualified ML tactic names. The plugin name is used to discriminate	Pierre-Marie Pédrot	2014-07-27
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Modulification of identifier	ppedrot	2012-12-14
*	Added support for option Local (at module level) in Tactic Notation.	herbelin	2012-08-11
*	Updating headers.	herbelin	2012-08-08
*	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey	2012-07-05
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
*	remove many excessive open Util & Errors in mli's	letouzey	2012-05-29
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	Slight change in the semantics of arguments scopes: scopes can no	herbelin	2012-03-26
*	Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic	herbelin	2012-03-20
*	Noise for nothing	pboutill	2012-03-02
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Simplified the way internalization_data (i.e. bindings of bound vars	herbelin	2010-07-22
*	New script dev/tools/change-header to automatically update Coq files headers.	herbelin	2010-06-22
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Move from ocamlweb to ocamdoc to generate mli documentation	pboutill	2010-04-29
*	Several bug-fixes and improvements of coqdoc	herbelin	2010-03-29
*	Restructuration of command.ml + generic infrastructure for inductive schemes	herbelin	2009-11-08
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	- Addition of "Reserved Infix" continued.	herbelin	2009-09-14
*	Generalized the possibility to refer to a global name by a notation	herbelin	2009-09-11
*	Add support for "Infix ... := constr" instead of just "Infix ... := ref".	herbelin	2009-08-11
*	- Cleaning (unification of ML names, removal of obsolete code,	herbelin	2009-04-27
*	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin	2008-10-19
*	Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)	herbelin	2007-02-24
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin	2005-12-26
*	Simplifification de vernac_expr li l'abandon du traducteur	herbelin	2005-12-23
*	Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...	herbelin	2005-05-17
*	Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...	herbelin	2005-01-02
*	Nouvelle en-tête	herbelin	2004-07-16
*	Traitement plus clair, notamment pour Locate, de quand quoter les composantes...	herbelin	2003-11-22
*	Changement 'as notation' en 'where notation'	herbelin	2003-10-14
*	Implantation de l'option 'format' des Notations	herbelin	2003-10-01
*	Ajout 'Close Scope'.	herbelin	2003-09-30
*	parsing	herbelin	2003-09-19
*	Ajout 'Print Scopes' et 'Bind Scope with classes'	herbelin	2003-09-12
*	Traduction de Distfix	herbelin	2003-09-10