coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Continuing experimentation on what part of the instance of an evar	Hugo Herbelin	2015-02-21
*	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	Reactivating option "Set Printing Existential Instances" for asking printing ...	Hugo Herbelin	2014-12-04
*	Printing function for [uconstr].	Arnaud Spiwack	2014-11-19
*	A patch for printing "match" when constructors are defined with let-in	Hugo Herbelin	2014-10-20
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Fix debug printing with primitive projections.	Matthieu Sozeau	2014-09-18
*	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau	2014-09-17
*	More on printing references applied to implicit arguments.	Hugo Herbelin	2014-09-16
*	Parsing evar instances.	Hugo Herbelin	2014-09-12
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	Parsing and printing of primitive projections, fix buggy behavior when	Matthieu Sozeau	2014-09-10
*	- Fix printing and parsing of primitive projections, including the Set	Matthieu Sozeau	2014-09-09
*	Fix bug #3591: print differently eta-expanded projection implicit application...	Matthieu Sozeau	2014-09-08
*	Parsing of Type@{max(i,j)}.	Matthieu Sozeau	2014-09-08
*	Spotted a source of failure of the constr printer in debugger.	Hugo Herbelin	2014-08-18
*	Fix non-printing of coercions for primitive projections (fixes bug #3433).	Matthieu Sozeau	2014-08-14
*	Change internalization of primitive projections to allow parsing [p t] as	Matthieu Sozeau	2014-08-08
*	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin	2014-08-01
*	Consistent pretty-printing of primitive projections and their expanded forms.	Matthieu Sozeau	2014-07-31
*	Fix printing of projections with implicits.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Never suppress the typing constraint of bound variables whose name was	Pierre-Marie Pédrot	2014-03-01
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	Now printing body of abbreviations (i.e. notation with a name) with	herbelin	2013-05-05
*	Robust display of NotConvertibleTypeField errors (fix #3008, #2995)	letouzey	2013-03-21
*	Restrict (try...with...) to avoid catching critical exn (part 8)	letouzey	2013-03-13
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Fixup notation printing in patterns	pboutill	2013-01-07
*	Modulification of identifier	ppedrot	2012-12-14
*	Implemented a full-fledged equality on [constr_expr]. By the way,	ppedrot	2012-12-14
*	Using library string functions.	ppedrot	2012-12-13
*	Renamed Option.Misc.compare to the more uniform Option.equal.	ppedrot	2012-12-13
*	Fix ocamldebug constr printer	pboutill	2012-11-28
*	Fixed a monomorphization error.	ppedrot	2012-11-26
*	Monomorphization (interp)	ppedrot	2012-11-25
*	Added a CString module.	ppedrot	2012-11-13
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Fixed bug #2895	ppedrot	2012-09-09
*	Updating headers.	herbelin	2012-08-08
*	Fixing bug #2835 (the rationale for printing notations was not	herbelin	2012-07-21
*	Fixup implicits in patterns & notations	pboutill	2012-07-20
*	Bug 2838: ExplApp in mutual inductive parameters	pboutill	2012-07-12