coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-09
\|\
\| *	Rename Lexer -> CLexer.	Pierre-Marie Pédrot	2016-05-09
* \|	Adopting the same rules for interpreting @, abbreviations and	Hugo Herbelin	2016-03-13
* \|	Supporting "(@foo) args" in patterns, where "@foo" has no arguments.	Hugo Herbelin	2016-03-13
* \|	Uniformizing the parsing of argument scopes in Ltac.	Pierre-Marie Pédrot	2016-03-04
* \|	Removing the METAIDENT token, as it is not used anymore.	Pierre-Marie Pédrot	2016-02-24
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	CLEANUP: removing unused field	Matej Kosik	2016-01-11
* \|	CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified	Matej Kosik	2015-12-18
\|/
*	Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.	Hugo Herbelin	2015-12-02
*	Record fields accept an optional final semicolon separator.	Pierre-Marie Pédrot	2015-10-07
*	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
*	Notation: use same level for "@" in constr: and pattern: (Close: #4272)	Enrico Tassi	2015-07-01
*	Inlining "fun" and "forall" tokens in parser, so that alternative notations for	Hugo Herbelin	2015-04-20
*	Fixing #3982 (conflict with max notation for universes).	Hugo Herbelin	2015-02-12
*	Update headers.	Maxime Dénès	2015-01-12
*	Parsing of "?[" as two tokens (makes ssr compile).	Enrico Tassi	2014-10-13
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Checking typability of evar instances. Using ";" to separate bindings	Hugo Herbelin	2014-09-13
*	Parsing evar instances.	Hugo Herbelin	2014-09-12
*	Parsing of Type@{max(i,j)}.	Matthieu Sozeau	2014-09-08
*	Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...	Matthieu Sozeau	2014-06-10
*	- Better parsing and printing of named universes: Type{ident} and foo@{(ident...	Matthieu Sozeau	2014-06-04
*	- Allow parsing of @const@{instance} for specifying universe instances of pol...	Matthieu Sozeau	2014-06-04
*	- Fix hashing of levels to get the "right" order in universe contexts etc...	Matthieu Sozeau	2014-06-04
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Actually adding the grammar entry to handle tactics in terms.	Pierre-Marie Pédrot	2013-11-27
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Compat to parsing. This permits to break the dependency of the	ppedrot	2012-10-04
*	avoid referring to Term in constrexpr.mli and glob_term.mli	letouzey	2012-10-02
*	Updating headers.	herbelin	2012-08-08
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Internalization of pattern is done in two phases.	pboutill	2012-06-14
*	Strongly reduce the dependencies of grammar.cma, modulo two hacks	letouzey	2012-05-29
*	Basic stuff about constr_expr migrated from topconstr to constrexpr_ops	letouzey	2012-05-29
*	Stuff about notation_constr (ex-aconstr) now in notation_ops.ml	letouzey	2012-05-29
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey	2012-05-29
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	"A -> B" is a notation for "forall _ : A, B".	pboutill	2012-04-12
*	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin	2012-04-06
*	Noise for nothing	pboutill	2012-03-02
*	In the syntax of pattern matching, "in" clauses are patterns.	pboutill	2012-02-29
*	Fix typeclass constraint grammar rule to allow `{_ : Reflexive A R}.	msozeau	2012-01-19
*	Add a syntax entry for fully applied constructor pattern	pboutill	2011-07-22
*	- Add modulo_delta_types flag for unification to allow full	msozeau	2011-03-13
*	Forgotten removal of ',' in 'fun' rule: it has to come with the lambda notation	herbelin	2011-03-05