coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Bump year in headers.	Maxime Dénès	2017-06-01
\|
*	AlistNsep token now accepts an arbitrary separator.	Pierre-Marie Pédrot	2016-05-10
\|
*	Simpler data structure for Arules token.	Pierre-Marie Pédrot	2016-05-10
\|
*	Removing the Entry module now that rules need not be marshalled.	Pierre-Marie Pédrot	2016-05-10
\|
*	Higher-level API for tactic notations.	Pierre-Marie Pédrot	2016-04-24
\|
*	Getting rid of the "_mods" parsing entry.	Pierre-Marie Pédrot	2016-04-01
\| \| \| \| \| \|	It was only used by setoid_ring for the Add Ring command, and was easily replaced by a dedicated argument. Moreover, it was of no use to tactic notations.
*	Allowing generalized rules in typed symbols.	Pierre-Marie Pédrot	2016-03-19
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| \|
* \|	Separating the parsing of user-defined entries from their intepretation.	Pierre-Marie Pédrot	2016-01-16
\| \|
* \|	Fixing the return type of the Atoken symbol.	Pierre-Marie Pédrot	2015-10-28
\| \|
* \|	Type-safe grammar extensions.	Pierre-Marie Pédrot	2015-10-27
\|/
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
\| \| \| \| \| \| \| \| \| \| \| \|	kernel on CAMLP4/5 structures, and consequently should also erase such structures from vo files. This modification requires some code duplication, mainly while reimplementing our own location data type. This is chiefly visible in the ml4 files, where CAMLP4/5 locations must be manually converted to our locations with an explicit (!@) cast operator. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
\| \| \| \| \| \| \| \| \| \|	were closed (i.e. the only remaining ones are those of printing/parsing). Meanwhile, a simplified interface is provided in loc.mli. This also permits to put Pp in Clib, because it does not depend on CAMLP4/5 anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extend become a mli-only file in intf/	letouzey	2012-05-29
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15390 85f007b7-540e-0410-9357-904b9bb8a0f7