coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Adding a variant get_truncation_family_of of get_sort_family_of.	Hugo Herbelin	2017-11-28
*	Use Evarutil.has_undefined_evars for tactic has_evar.	Gaëtan Gilbert	2017-11-24
*	Merge PR #6197: [plugin] Remove LocalityFixme über hack.	Maxime Dénès	2017-11-24
\|\
* \	Merge PR #6186: [api] Miscellaneous consolidation.	Maxime Dénès	2017-11-23
\|\ \
* \ \	Merge PR #6200: Remove pidentref grammar entry.	Maxime Dénès	2017-11-23
\|\ \ \
\| \| \| *	[plugin] Remove LocalityFixme über hack.	Emilio Jesus Gallego Arias	2017-11-22
\| \| \| *	[plugin] Encapsulate modifiers to vernac commands.	Emilio Jesus Gallego Arias	2017-11-22
\| \|_\|/ \|/\| \|
\| \| *	[api] Re-enable deprecation warnings.	Emilio Jesus Gallego Arias	2017-11-22
\| \| *	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
\| \| *	[api] Miscellaneous consolidation + moves to engine.	Emilio Jesus Gallego Arias	2017-11-21
\| \|/ \|/\|
* \|	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
* \|	Merge PR #6185: [parser] Remove unnecessary statically initialized hook.	Maxime Dénès	2017-11-21
\|\ \
* \ \	Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API.	Maxime Dénès	2017-11-21
\|\ \ \
\| \| \| *	Remove pidentref grammar entry.	Gaëtan Gilbert	2017-11-20
\| \|_\|/ \|/\| \|
\| \| *	[parser] Remove unnecessary statically initialized hook.	Emilio Jesus Gallego Arias	2017-11-19
* \| \|	[plugins] Prepare plugin API for functional handling of state.	Emilio Jesus Gallego Arias	2017-11-19
\| \|/ \|/\|
\| *	[proof] Attempt to deprecate some V82 parts of the proof API.	Emilio Jesus Gallego Arias	2017-11-19
\|/
*	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias	2017-11-13
*	[ci] [coq] Complete 4.06.0 support.	Emilio Jesus Gallego Arias	2017-11-13
*	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] Remove 8.7 ML-deprecated functions.	Emilio Jesus Gallego Arias	2017-11-07
\| \| *	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
\| \|/ \|/\|
* \|	Merge PR #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" ...	Maxime Dénès	2017-11-06
\|\ \
* \| \|	Setting a system to register printers for Ltac values.	Hugo Herbelin	2017-11-02
* \| \|	Using a specific function to register vernac printers.	Hugo Herbelin	2017-11-02
\| \| *	[API] Some reordering following latest separation commits.	Emilio Jesus Gallego Arias	2017-11-01
\| \|/ \|/\|
\| *	provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules	Matej Košík	2017-11-01
\|/
*	Merge PR #6015: [general] Remove Econstr dependency from `intf`	Maxime Dénès	2017-10-27
\|\
* \|	Passing around the flag for injection so that tactics calling inj at	Hugo Herbelin	2017-10-26
\| *	[general] Remove Econstr dependency from `intf`	Emilio Jesus Gallego Arias	2017-10-25
\|/
*	[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
*	[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
*	[vernac] Remove "Proof using" hacks from parser.	Emilio Jesus Gallego Arias	2017-10-10
*	Merge PR #768: Omega and romega know about context definitions (fix old bug 148)	Maxime Dénès	2017-10-10
\|\
* \	Merge PR #1087: [stm] Switch to a functional API	Maxime Dénès	2017-10-09
\|\ \
\| * \|	[stm] Switch to a functional API	Emilio Jesus Gallego Arias	2017-10-06
\| \| *	romega: takes advantage of context variables with body	Pierre Letouzey	2017-10-05
\| \|/
* \|	Ltac uses the new generic locatable API.	Pierre-Marie Pédrot	2017-10-03
* \|	Moving the Ltac-specific part of the nametab to the Ltac plugin.	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
\|\
* \|	Remove STM vernaculars.	Maxime Dénès	2017-09-19
\| *	Don't lose names in UState.universe_context.	Gaëtan Gilbert	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
\|\