coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
*	Glob_ops: cosmetic renaming to reflect the type of objects.	Hugo Herbelin	2018-03-28
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Using an "as" clause when needed for printing irrefutable patterns.	Hugo Herbelin	2018-02-20
*	Adding patterns in the category of binders for notations.	Hugo Herbelin	2018-02-20
*	Canonically add an encoding in glob_constr of "as" operator for cases_pattern.	Hugo Herbelin	2018-02-20
*	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin	2018-02-20
*	Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-01-30
*	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
*	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
*	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
*	Fixing #5749 (bug in fold_constr_with_binders introduced in 4e70791).	Hugo Herbelin	2017-09-23
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	A fix to #5414 (ident bound by ltac names now known for "match").	Hugo Herbelin	2017-06-09
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-06-08
\|\
* \	Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...	Maxime Dénès	2017-06-05
\|\ \
* \ \	Merge PR#561: Improving the Name API	Maxime Dénès	2017-06-01
\|\ \ \
\| \| * \|	Using a more explicit algebraic type for evars of kind "MatchingVar".	Hugo Herbelin	2017-05-31
\| * \| \|	Creating a module Nameops.Name extending module Names.Name.	Hugo Herbelin	2017-05-31
\| \|/ /
* / /	Fixing #5523 (missing support for complex constructions in recursive notations).	Hugo Herbelin	2017-05-31
\|/ /
* \|	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \
\| * \|	Remove dead code and unused open.	Maxime Dénès	2017-05-05
* \| \|	[location] [ast] Port module AST to CAst	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] Make location optional in Loc.located	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] Switch glob_constr to Loc.located	Emilio Jesus Gallego Arias	2017-04-24
* \| \|	[location] Move Glob_term.predicate_pattern to located.	Emilio Jesus Gallego Arias	2017-04-24
* \| \|	[location] Move Glob_term.cases_pattern to located.	Emilio Jesus Gallego Arias	2017-04-24
\| * \|	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
\|/ /
\| *	Better support for printing constructors with let-ins.	Hugo Herbelin	2017-04-07
* \|	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