coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|\ \ \
* \ \ \	Merge PR #1048: Port is_Set and is_Type to EConstr, as was is_Prop already.	Maxime Dénès	2017-09-15
\|\ \ \ \
* \ \ \ \	Merge PR #1037: Parse directly to Sorts.family when appropriate.	Maxime Dénès	2017-09-15
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" In...	Maxime Dénès	2017-09-15
\|\ \ \ \ \ \
\| \| \| \| * \| \|	Using an algebraic type for distinguishing toplevel input from location in file.	Hugo Herbelin	2017-09-14
\| \|_\|_\|/ / / \|/\| \| \| \| \|
\| \| \| \| \| *	A possible fix for BZ#5715 (escape non-utf8 win32 file names).	Hugo Herbelin	2017-09-13
* \| \| \| \| \|	Fixing bug #5693 (treating empty notation format as any format).	Hugo Herbelin	2017-09-12
\| \|_\|_\|_\|/ \|/\| \| \| \|
\| \| \| * \|	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
\| \|/ / \|/\| \|
* \| \|	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
* \| \|	Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name	Maxime Dénès	2017-08-31
\|\ \ \