coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06
*	Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.	Maxime Dénès	2017-11-06
\|\
* \	Merge PR #6063: Finish removing Show Goal uid	Maxime Dénès	2017-11-06
\|\ \
\| \| *	[api] Deprecate all legacy uses of Name.Id in core.	Emilio Jesus Gallego Arias	2017-11-04
\| * \|	Finish removing Show Goal uid	Gaëtan Gilbert	2017-11-04
\| \|/
* /	provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules	Matej Košík	2017-11-01
\|/
*	Merge PR #677: Trunk+abstracting injection flags	Maxime Dénès	2017-10-27
\|\
\| *	Passing around the flag for injection so that tactics calling inj at	Hugo Herbelin	2017-10-26
* \|	Removing dead code which raised questions.	Hugo Herbelin	2017-10-24
\|/
*	Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...	Maxime Dénès	2017-10-20
\|\
* \|	[vernac] [state] Cache freeze/unfreeze	Emilio Jesus Gallego Arias	2017-10-17
* \|	[stm] Remove state-handling from Futures.	Emilio Jesus Gallego Arias	2017-10-17
* \|	[stm] Move interpretation state to Vernacentries	Emilio Jesus Gallego Arias	2017-10-17
* \|	Parse [Proof using Type] without translating Type to an id.	Gaëtan Gilbert	2017-10-10
* \|	Use a nice printer for constant names in Suggest Proof Using.	Gaëtan Gilbert	2017-10-10
* \|	Code factorization Vernacentries.interp on VernacProof.	Gaëtan Gilbert	2017-10-10
* \|	[vernac] Remove "Proof using" hacks from parser.	Emilio Jesus Gallego Arias	2017-10-10
* \|	Take Suggest Proof Using outside the kernel.	Gaëtan Gilbert	2017-10-10
* \|	Merge PR #1053: [deps] Move `Discharge` to `interp`	Maxime Dénès	2017-10-10
\|\ \
* \ \	Merge PR #1114: Generic handling of nameable objects for plugins	Maxime Dénès	2017-10-09
\|\ \ \
\| \| * \|	[deps] Move `Discharge` to `interp`	Emilio Jesus Gallego Arias	2017-10-09
* \| \| \|	Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on...	Maxime Dénès	2017-10-09
\|\ \ \ \ \| \|_\|/ / \|/\| \| \|
* \| \| \|	Merge PR #1121: Fixing BZ#5765 (an anomaly with 'pat in the parameters of an ...	Maxime Dénès	2017-10-06
\|\ \ \ \
* \ \ \ \	Merge PR #1081: Mini fix at improving the cannot unify error message	Maxime Dénès	2017-10-05
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 t...	Maxime Dénès	2017-10-05
\|\ \ \ \ \ \
\| \| \| * \| \| \|	Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).	Hugo Herbelin	2017-10-05
\| \| \| \| \| \| *	Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).	Hugo Herbelin	2017-10-05
\| \| \| \| \|_\|/ \| \| \| \|/\| \|
\| \| \| \| \| *	Implementing a generic mechanism for locating named objects from Coq side.	Pierre-Marie Pédrot	2017-10-03
\| \|_\|_\|_\|/ \|/\| \| \| \|
* \| \| \| \|	Merge PR #1040: Efficient fresh name generation	Maxime Dénès	2017-10-03
\|\ \ \ \ \
* \| \| \| \| \|	[vernac] Remove `Qed exporting` syntax.	Emilio Jesus Gallego Arias	2017-09-29
\| \|_\|_\|/ / \|/\| \| \| \|
\| * \| \| \|	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
\|/ / / /
* \| \| \|	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès	2017-09-26
\|\ \ \ \
\| \| \| \| *	BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations	Paul Steckler	2017-09-25
* \| \| \| \|	Merge PR #1085: Fix BZ#5755 (incorrect treatment of let-ins in parameters of ...	Maxime Dénès	2017-09-25
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #1057: Reporting locations in error messages about notation formats.	Maxime Dénès	2017-09-25
\|\ \ \ \ \ \
\| \| * \| \| \| \|	Discharge.ml: cosmetic renaming of some variables.	Hugo Herbelin	2017-09-23
\| \| * \| \| \| \|	Fixing #5755 (discharging of inductive types not correct with let-ins).	Hugo Herbelin	2017-09-23
\| \|/ / / / / \|/\| \| \| \| \|
\| \| \| \| * \|	Himsg: Dropping nf_evars made obsolete by EConstr.	Hugo Herbelin	2017-09-22
\| \| \| \| * \|	Cannot unify message: improve preventing repeating twice the same message.	Hugo Herbelin	2017-09-22
\| \| \| \| \|/
* \| \| \| \|	Merge PR #1055: Remove STM vernaculars	Maxime Dénès	2017-09-22
\|\ \ \ \ \
* \| \| \| \| \|	[flags] Flag `open Flags`	Emilio Jesus Gallego Arias	2017-09-20
\| \|_\|_\|_\|/ \|/\| \| \| \|
\| * \| \| \|	Remove STM vernaculars.	Maxime Dénès	2017-09-19
\|/ / / /
\| \| * \|	Don't lose names in UState.universe_context.	Gaëtan Gilbert	2017-09-19
\| \| * \|	proof_global: cleanup and comment close_proof	Matthieu Sozeau	2017-09-19
\| \| * \|	Allow declaring universe constraints at definition level.	Matthieu Sozeau	2017-09-19
\| \|/ / \|/\| \|
\| * \|	Reporting locations in error messages about notation formats.	Hugo Herbelin	2017-09-18
\| * \|	Fixing two anomalies in corner cases of the syntax of notation formats.	Hugo Herbelin	2017-09-18
\|/ /
* \|	Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ...	Maxime Dénès	2017-09-15
\|\ \
* \ \	Merge PR #1051: Using an algebraic type for distinguishing toplevel input fro...	Maxime Dénès	2017-09-15
\|\ \ \