coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Allow local universe renaming in Print.	Gaëtan Gilbert	2017-11-25
*	Finish removing Show Goal uid	Gaëtan Gilbert	2017-11-04
*	[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
\| *	[vernac] Store Infix Modifier in Vernac Notation.	Pierre-Marie Pédrot	2017-08-29
\|/
*	Improve errors for cumulativity when monomorphic	Amin Timany	2017-07-31
*	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
\|/
*	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
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07