coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[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 general support for irrefutable disjunctive patterns.	Hugo Herbelin	2018-02-20
*	Respecting the ident/pattern distinction in notation modifiers.	Hugo Herbelin	2018-02-20
*	Adding support for parsing subterms of a notation as "pattern".	Hugo Herbelin	2018-02-20
*	Allows recursive patterns for binders to be associative on the left.	Hugo Herbelin	2018-02-20
*	A bit of miscellaneous code documentation around notations.	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
*	Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.	Hugo Herbelin	2018-02-20
*	More precise explanation when a notation is not reversible for printing.	Hugo Herbelin	2018-02-20
*	Merge PR #6651: Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-02-12
\|\
* \|	[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
\|/
*	Merge PR #6499: [vernac] Move the flags/attributes out of vernac_expr	Maxime Dénès	2018-01-16
\|\
\| *	[vernac] vernac_expr no longer recursive	Vincent Laporte	2018-01-08
* \|	Brackets support single numbered goal selectors.	Théo Zimmermann	2018-01-05
\| *	[vernac] Define types in order	Vincent Laporte	2017-12-29
\|/
*	Merge PR #6433: [flags] Move global time flag into an attribute.	Maxime Dénès	2017-12-29
\|\
* \|	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
\| *	[flags] Move global time flag into an attribute.	Emilio Jesus Gallego Arias	2017-12-23
\|/
*	Separate vernac controls and regular commands.	Maxime Dénès	2017-12-20
*	Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...	Maxime Dénès	2017-12-14
\|\
\| *	In printing, factorizing "match" clauses with same right-hand side.	Hugo Herbelin	2017-12-12
\| *	Removing cumbersome location in multiple patterns.	Hugo Herbelin	2017-12-12
* \|	Merge PR #1150: [stm] Remove all but one use of VtUnknown.	Maxime Dénès	2017-12-11
\|\ \
* \| \|	[api] Remove kernel dependency on intf (Decl_kind)	Emilio Jesus Gallego Arias	2017-12-10
\| \|/ \|/\|
\| *	[stm] Remove all but one use of VtUnknown.	Emilio Jesus Gallego Arias	2017-12-09
\|/
*	Proper nametab handling of global universe names	Matthieu Sozeau	2017-12-01
*	Remove "obsolete_locality" and fix STM vernac classification.	Maxime Dénès	2017-11-29
*	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\
* \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
\| *	Allow local universe renaming in Print.	Gaëtan Gilbert	2017-11-25
\|/
*	Merge PR #6098: [api] Move structures deprecated in the API to the core.	Maxime Dénès	2017-11-13
\|\
* \	Merge PR #6052: [general] Move Tactypes to `interp` + API reordering.	Maxime Dénès	2017-11-13
\|\ \
\| \| *	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\| \|/ \|/\|
* \|	Finish removing Show Goal uid	Gaëtan Gilbert	2017-11-04
\| *	[general] Move Tactypes to `interp`	Emilio Jesus Gallego Arias	2017-11-01
\|/
*	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
*	[stm] Remove VtBack from public classification.	Emilio Jesus Gallego Arias	2017-10-17
*	[stm] First step to move interpretation of Undo commands out of the classifier.	Emilio Jesus Gallego Arias	2017-10-17
*	Parse [Proof using Type] without translating Type to an id.	Gaëtan Gilbert	2017-10-10
*	Implementing a generic mechanism for locating named objects from Coq side.	Pierre-Marie Pédrot	2017-10-03
*	[vernac] Remove `Qed exporting` syntax.	Emilio Jesus Gallego Arias	2017-09-29
*	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès	2017-09-26
\|\
* \|	Remove STM vernaculars.	Maxime Dénès	2017-09-19
\| *	Allow declaring universe constraints at definition level.	Matthieu Sozeau	2017-09-19
\|/