coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	More {raw => glob} changes for consistency	glondu	2010-12-24
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	r13359 continued: removed native treatment for λ (lambda) and Π (Pi)	herbelin	2010-07-30
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	Constrintern: unified push_name_env and push_loc_name_env; made	herbelin	2010-07-22
*	Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).	herbelin	2010-07-22
*	Add (almost) compatibility with camlp4, without breaking support for camlp5	letouzey	2010-05-19
*	Nicer representation of tokens, more independant of camlp*	letouzey	2010-05-19
*	static (and shared) camlp4use instead of per-file declaration	letouzey	2010-05-19
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Added support for definition of fixpoints using tactics.	herbelin	2009-11-27
*	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio	2009-11-04
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	- Cleaning (unification of ML names, removal of obsolete code,	herbelin	2009-04-27
*	Some dead code removal + cleanups	letouzey	2009-04-08
*	Avoid inadvertent declaration of "on" as a keyword. New syntax is	msozeau	2009-03-29
*	Rewrite of Program Fixpoint to overcome the previous limitations:	msozeau	2009-03-28
*	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau	2008-12-14
*	More factorization of inductive/record and typeclasses: move class	msozeau	2008-11-09
*	Move Record desugaring to constrintern and add ability to use notations	msozeau	2008-11-05