coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove dead code and unused open.	Maxime Dénès	2017-05-05
*	Using fold_glob_constr_with_binders to code bound_glob_vars.	Hugo Herbelin	2017-04-13
*	Adding a fold_glob_constr_with_binders combinator.	Hugo Herbelin	2017-04-13
*	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24
*	A new step on using alpha-conversion in printing notations.	Hugo Herbelin	2016-07-18
*	Partial fix to #4592 (notation requiring alpha-conversion for printing).	Hugo Herbelin	2016-07-17
*	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Fixing #4677 (collision of a global variable and of a local variable	Hugo Herbelin	2016-04-19
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Fixing untimely unexpected warning "Collision between bound variables" (#4317).	Hugo Herbelin	2015-10-11
*	Fixing obviously untested fold_glob_constr and iter_glob_constr.	Hugo Herbelin	2015-10-11
*	Update headers.	Maxime Dénès	2015-01-12
*	Printing function for [uconstr].	Arnaud Spiwack	2014-11-19
*	Glob-ops: a name-mapping operation for pattern-matching binders.	Arnaud Spiwack	2014-11-19
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau	2014-09-17
*	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
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code	Pierre Letouzey	2014-03-02
*	Adding an equality function over glob_constr	Pierre-Marie Pédrot	2014-03-02
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Modulification of identifier	ppedrot	2012-12-14
*	Added a constr_pattern_eq	ppedrot	2012-11-23
*	Monomorphization (pretyping)	ppedrot	2012-11-22
*	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
*	Updating headers.	herbelin	2012-08-08
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Glob_term now mli-only, operations now in Glob_ops	letouzey	2012-05-29