coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7384: Split Universes	Pierre-Marie Pédrot	2018-05-22
\|\
* \	Merge PR #6965: [api] Move universe syntax to `Glob_term`	Pierre-Marie Pédrot	2018-05-18
\|\ \
\| \| *	Split off Universes functions dealing with names.	Gaëtan Gilbert	2018-05-17
\| \|/ \|/\|
* \|	Merge PR #7340: Remove DirClosedSection.	Enrico Tassi	2018-05-11
\|\ \
\| \| *	[api] Move universe syntax to `Glob_term`	Emilio Jesus Gallego Arias	2018-05-08
\| \|/ \|/\|
* \|	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
* \|	Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.	Pierre-Marie Pédrot	2018-05-04
\|\ \
* \| \|	[api] Move bullets and goals selectors to `proofs/`	Emilio Jesus Gallego Arias	2018-05-01
\| * \|	[api] Move `hint_info_expr` to `Typeclasses`.	Emilio Jesus Gallego Arias	2018-04-26
\|/ /
\| *	Remove DirClosedSection.	Jasper Hugunin	2018-04-24
\|/
*	Merge PR #7152: [api] Remove dependency of library on Vernacexpr.	Pierre-Marie Pédrot	2018-04-23
\|\
* \|	Evar maps contain econstrs.	Gaëtan Gilbert	2018-04-13
\| *	[api] Remove dependency of library on Vernacexpr.	Emilio Jesus Gallego Arias	2018-04-06
\|/
*	Merge PR #7016: Make parsing independent of the cumulativity flag.	Enrico Tassi	2018-04-05
\|\
* \	Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.	Enrico Tassi	2018-04-04
\|\ \
\| * \|	[stm] Move VernacBacktrack to the toplevel.	Emilio Jesus Gallego Arias	2018-04-01
* \| \|	Remove deprecated commands Arguments Scope and Implicit Arguments	Jasper Hugunin	2018-03-30
\|/ /
\| *	bool option -> (VernacCumulative \| VernacNonCumulative) option	Gaëtan Gilbert	2018-03-22
\| *	Make parsing independent of the cumulativity flag.	Gaëtan Gilbert	2018-03-21
* \|	[vernac] Move `Quit` and `Drop` to the toplevel layer.	Emilio Jesus Gallego Arias	2018-03-11
\|/
*	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias	2018-03-09
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	Implement the Export Set/Unset feature.	Pierre-Marie Pédrot	2018-03-09
*	Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials	Maxime Dénès	2018-03-08
\|\
* \	Merge PR #6893: Cleanup UState API usage	Maxime Dénès	2018-03-08
\|\ \
* \ \	Merge PR #6790: Allow universe declarations for [with Definition].	Maxime Dénès	2018-03-07
\|\ \ \
\| \| * \|	Deprecate UState aliases in Evd.	Gaëtan Gilbert	2018-03-06
\| \|/ / \|/\| \|
\| * \|	Allow universe declarations for [with Definition].	Gaëtan Gilbert	2018-03-05
* \| \|	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\ \ \ \| \|/ / \|/\| \|
* \| \|	Merge PR #6736: [toplevel] Move beautify to its own pass.	Maxime Dénès	2018-03-04
\|\ \ \
\| * \| \|	[toplevel] Move beautify to its own pass.	Emilio Jesus Gallego Arias	2018-02-28
* \| \| \|	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias	2018-02-28
\|/ / /
\| * /	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/ /
\| *	Adding mention of shelved/given-up status in "Show Existentials".	Hugo Herbelin	2018-02-22
* \|	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
\|/
*	Change default for notations with variables bound to both terms and binders.	Hugo Herbelin	2018-02-20
*	Notations: Adding modifiers to tell which kind of binder a constr can parse.	Hugo Herbelin	2018-02-20
*	Notations: A step in cleaning constr_entry_key.	Hugo Herbelin	2018-02-20
*	Adding support for parsing subterms of a notation as "pattern".	Hugo Herbelin	2018-02-20
*	Introducing an intermediary type "constr_prod_entry_key" for grammar producti...	Hugo Herbelin	2018-02-20
*	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin	2018-02-20
*	Merge PR #1082: Fixing Print for inductive types with let-in in parameters	Maxime Dénès	2018-02-12
\|\
* \	Merge PR #6128: Simplification: cumulativity information is variance informa...	Maxime Dénès	2018-02-12
\|\ \
* \ \	Merge PR #6651: Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-02-12
\|\ \ \
\| \| * \|	Print inductive cumulativity info in About.	Gaëtan Gilbert	2018-02-11
\| \| * \|	Simplification: cumulativity information is variance information.	Gaëtan Gilbert	2018-02-10
\| \|/ / \|/\| \|
* \| \|	[vernac] Mutual theorems (VernacStartTheoremProof) always have names	Vincent Laporte	2018-02-01
* \| \|	[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition	Vincent Laporte	2018-02-01
\| * \|	Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-01-30
\|/ /
* \|	[printing] Remove duplicate definitions of pr_lident and pr_lname	Vincent Laporte	2018-01-22