coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[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
\| *	Merge PR#582: Fix warnings	Maxime Dénès	2017-05-02
\| \|\
\| * \|	Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"."	Maxime Dénès	2017-04-28
\| * \|	Using a more explicit algebraic type for evars of kind "MatchingVar".	Hugo Herbelin	2017-04-28
\| * \|	Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...	Maxime Dénès	2017-04-28
\| \|\ \
\| \| \| *	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
\| \| \|/ \| \|/\|
* \| \|	[location] [ast] Port module AST to CAst	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] [ast] Switch Constrexpr AST to an extensible node type.	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] Be consistent with type module qualification	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] Use located in misctypes.	Emilio Jesus Gallego Arias	2017-04-24
* \| \|	[location] More located use.	Emilio Jesus Gallego Arias	2017-04-24