coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[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
\|\
* \	Merge PR #1051: Using an algebraic type for distinguishing toplevel input fro...	Maxime Dénès	2017-09-15
\|\ \
* \ \	Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.	Maxime Dénès	2017-09-15
\|\ \ \
\| \| * \|	Using an algebraic type for distinguishing toplevel input from location in file.	Hugo Herbelin	2017-09-14
\| * \| \|	Port is_Set and is_Type to EConstr, as was is_Prop already.	Guillaume Melquiond	2017-09-12
\| \|/ /
* / /	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert	2017-09-08
\|/ /
* \|	Merge PR #931: Parametrize module body	Maxime Dénès	2017-09-07
\|\ \
* \ \	Merge PR #914: Making the detyper lazy	Maxime Dénès	2017-09-07
\|\ \ \
* \ \ \	Merge PR #904: Add build_coq_or to API.Coqlib	Maxime Dénès	2017-09-07
\|\ \ \ \
\| \| * \| \|	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
\| \|/ / / \|/\| \| \|
\| \| \| *	[general] Merge parsing with highparsing, put toplevel at the top of the link...	Emilio Jesus Gallego Arias	2017-08-29
\| \| \| *	[vernac] Store Infix Modifier in Vernac Notation.	Pierre-Marie Pédrot	2017-08-29
\| \|_\|/ \|/\| \|
\| \| *	Statically enforcing that module types have no retroknowledge.	Pierre-Marie Pédrot	2017-08-29
\| \| *	Separating the module_type and module_body types by using a type parameter.	Pierre-Marie Pédrot	2017-08-29
\| \|/ \|/\|
* \|	Post-merge API fix.	Maxime Dénès	2017-08-29
* \|	Merge PR #946: Functional pretyping interface	Maxime Dénès	2017-08-29
\|\ \
* \ \	Merge PR #916: Fixing notation bug 5608 involving { } and a slight restructur...	Maxime Dénès	2017-08-29
\|\ \ \
* \ \ \	Merge PR #805: Functional tactics	Maxime Dénès	2017-08-29
\|\ \ \ \
\| \| * \| \|	A new step of restructuration of notations.	Hugo Herbelin	2017-08-29
\| \|/ / / \|/\| \| \|