coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|/
*	Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ...	Maxime Dénès	2017-09-15
\|\
* \|	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert	2017-09-08
* \|	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
\| *	[vernac] Store Infix Modifier in Vernac Notation.	Pierre-Marie Pédrot	2017-08-29
\|/
*	A new step of restructuration of notations.	Hugo Herbelin	2017-08-29
*	A little reorganization of notations + a fix to #5608.	Hugo Herbelin	2017-08-29
*	Merge PR #864: Some cleanups after cumulativity for inductive types	Maxime Dénès	2017-08-16
\|\
\| *	Improve errors for cumulativity when monomorphic	Amin Timany	2017-07-31
* \|	Adding support for recursive notations of the form "x , .. , y , z".	Hugo Herbelin	2017-07-26
\|/
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	[vernac] Remove stale bool parameter from `VernacStartTheoremProof`	Emilio Jesus Gallego Arias	2017-06-21
*	Merge PR#774: [ide] Add route_id parameter to query call.	Maxime Dénès	2017-06-20
\|\
\| *	[ide] Add route_id parameter to query call.	Emilio Jesus Gallego Arias	2017-06-18
* \|	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
\|/
*	Merge PR#719: Constrexpr.Numeral without bigint	Maxime Dénès	2017-06-15
\|\
* \	Merge PR#765: Remove obsolete Show commands	Maxime Dénès	2017-06-14
\|\ \
\| \| *	Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)	Pierre Letouzey	2017-06-14
\| * \|	Remove Show Thesis command which was never implemented.	Théo Zimmermann	2017-06-12
\| * \|	Remove non-working Show Tree and Show Node commands.	Théo Zimmermann	2017-06-12
\| * \|	Remove Show Implicit Arguments command.	Théo Zimmermann	2017-06-12
\| \|/
* /	A fix to #5414 (ident bound by ltac names now known for "match").	Hugo Herbelin	2017-06-09
\|/
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...	Maxime Dénès	2017-06-05
\|\
\| *	Using a more explicit algebraic type for evars of kind "MatchingVar".	Hugo Herbelin	2017-05-31
* \|	Support for using type information to infer more precise evar sources.	Hugo Herbelin	2017-05-30
\|/
*	[location] Renaming "CAst.ast" to "CAst.t"	Matej Košík	2017-05-24
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	[vernac] Remove `Save thm id.` command.	Emilio Jesus Gallego Arias	2017-05-23
\| *	[interp] [ast] Make raw_cases_pattern_expr private.	Emilio Jesus Gallego Arias	2017-05-15
\| *	Allow flexible anonymous universes in instances and sorts.	Gaetan Gilbert	2017-05-03