coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map	Hugo Herbelin	2017-08-29
\| \| \| \|	(from module List).
*	Merge PR #912: Detyping functions are now operating on EConstr.t.	Maxime Dénès	2017-08-16
\|\
* \	Merge PR #841: Timorous fix of bug #5598 on global existing class in sections	Maxime Dénès	2017-08-16
\|\ \
* \ \	Merge PR #864: Some cleanups after cumulativity for inductive types	Maxime Dénès	2017-08-16
\|\ \ \
\| \| \| *	Detyping functions are now operating on EConstr.t.	Pierre-Marie Pédrot	2017-08-01
\| \|_\|/ \|/\| \| \| \| \| \| \| \|	This was already the case, but the API was not exposing this.
* \| \|	Merge PR #919: Remove a few useless evar-normalizations in printing code.	Maxime Dénès	2017-08-01
\|\ \ \
* \ \ \	Merge PR #834: Adding support for recursive notations of the form "x , .. , ↵	Maxime Dénès	2017-08-01
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	y , z".
\| \| \| * \|	Improve errors for cumulativity when monomorphic	Amin Timany	2017-07-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We now only issue an error for locally specified (non)cumulativity whenever it is the context (set locally or globally) is monorphic.
\| \| \| * \|	Change the option for cumulativity	Amin Timany	2017-07-31
\| \| \| \| \|
\| \| \| * \|	Issue error on monomorphic cumulative inductives	Amin Timany	2017-07-31
\| \| \| \| \|
* \| \| \| \|	Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead	Maxime Dénès	2017-07-31
\|\ \ \ \ \ \| \|_\|_\|/ / \|/\| \| \| \|
\| * \| \| \|	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\| \| \| \| \|
\| \| \| * \|	Remove a few useless evar-normalizations in printing code.	Pierre-Marie Pédrot	2017-07-26
\| \| \|/ / \| \|/\| \|
* \| \| \|	Removing template polymorphism for definitions.	Pierre-Marie Pédrot	2017-07-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The use of template polymorphism in constants was quite limited, as it only applied to definitions that were exactly inductive types without any parameter whatsoever. Furthermore, it seems that following the introduction of polymorphic definitions, the code path enforced regular polymorphism as soon as the type of a definition was given, which was in practice almost always. Removing this feature had no observable effect neither on the test-suite, nor on any development that we monitor on Travis. I believe it is safe to assume it was nowadays useless.
* \| \| \|	Statically ensuring that inlined entries out of the kernel have no effects.	Pierre-Marie Pédrot	2017-07-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was an easy to prove property that I somehow overlooked.
* \| \| \|	More precise type for universe entries.	Pierre-Marie Pédrot	2017-07-26
\|/ / / \| \| \| \| \| \| \| \| \| \| \| \|	We use an algebraic type instead of a pair of a boolean and the corresponding data. For now, this is isomorphic, but this allows later change in the structure.
\| * /	Adding support for recursive notations of the form "x , .. , y , z".	Hugo Herbelin	2017-07-26
\|/ / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Since camlp5 parses from left, the last ", z" was parsed as part of an arbitrary long list of "x1 , .. , xn" and a syntax error was raised since an extra ", z" was still expected. We support this by translating "x , .. , y , z" into "x , y , .. , z" and reassembling the arguments appropriately after parsing.
* \|	Merge PR #899: [general] Move files to directories so they match linking order.	Maxime Dénès	2017-07-20
\|\ \
* \ \	Merge branch 'v8.7'	Maxime Dénès	2017-07-20
\|\ \ \
* \ \ \	Merge PR #770: [proof] Move bullets to their own module.	Maxime Dénès	2017-07-19
\|\ \ \ \
\| \| \| * \|	[general] Move files to directories matching linking order.	Emilio Jesus Gallego Arias	2017-07-19
\| \|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`, `Miscprint`) to their proper place as they were declared in different `mllib` files than the one in their directory. In some cases this could be refined but we don't do anything fancy, we just reflect the status quo.
* \| \| \|	Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers	Maxime Dénès	2017-07-17
\|\ \ \ \
* \ \ \ \	Merge PR #862: Adding support for bindings tags to explicit prefix/suffix ↵	Maxime Dénès	2017-07-17
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	rather than colors
\| \| * \| \| \|	Removing the uses of abstraction-breaking code in Lemmas.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	I had to slightly tweak a test in order to work around a bug of simpl that loses universes constraints when refolding polymorphic fixpoints.
\| \| * \| \| \|	Removing the uses of abstraction-breaking code in Obligations.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| \|
\| \| * \| \| \|	Remove the function Global.type_of_global_unsafe.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| \|
\| \| * \| \| \|	The only abstraction-breaking function in Univ is now AUContext.instance.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| \|
\| \| * \| \| \|	Getting rid of AUContext abstraction breakers in Discharge.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| \|
\| \| * \| \| \|	Make the typeclass implementation fully compatible with universe polymorphism.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This essentially means storing the abstract universe context in the typeclass data, and abstracting it when necessary.
\| \| * \| \| \|	Safer API for Global.body_of_constant and variants.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We aditionally return the abstract universe context inside the option. This is relatively painless as most uses were using the option as a boolean.
\| \| * \| \| \|	Safer API for Global.type_of_global_in_context.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We return the abstract context instead of an arbitrary instantiation.
\| \| * \| \| \|	Getting rid of AUContext abstraction breakers in Record.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| \|
\| \| * \| \| \|	Getting rid of AUContext abstraction breakers in Search.	Pierre-Marie Pédrot	2017-07-13
\| \|/ / / / \|/\| \| \| \|
\| \| \| * \|	Deprecate options that were introduced for compatibility with 8.5.	Théo Zimmermann	2017-07-11
\| \| \| \| \|
* \| \| \| \|	Properly handling polymorphic inductive subtyping in the kernel.	Pierre-Marie Pédrot	2017-07-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Before this patch, inductive subtyping was enforcing syntactic equality of the variable instance, instead of reasoning up to alpha-renaming.
* \| \| \| \|	Safe API for accessing universe constraints of global references.	Pierre-Marie Pédrot	2017-07-11
\| \|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel.
\| * \| \|	Adding support for bindings tags to explicit prefix/suffix rather than colors.	Hugo Herbelin	2017-07-08
\|/ / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is usable for no-color terminal. For instance, a typical application in mind is the Coq-generate names marker which can be rendered with a color if the interface supports it and a prefix "~" if the interface does not support colors.
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-07-04
\| \| \|
* \| \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\| \| \|
\| \| *	Preparing to hints supporting discharge.	Hugo Herbelin	2017-06-27
\| \|/ \|/\| \| \| \| \| \| \|	I.e., do not set local flag to false when in a section since compatibility tells discharge of hints is not supported.
* \|	Merge PR#821: [vernac] Remove stale bool parameter from ↵	Maxime Dénès	2017-06-23
\|\ \ \| \| \| \| \| \| \| \| \|	`VernacStartTheoremProof`
\| * \|	[vernac] Remove stale bool parameter from `VernacStartTheoremProof`	Emilio Jesus Gallego Arias	2017-06-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	`VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today.
* \| \|	[vernac] Remove forward hooks from Obligations.	Emilio Jesus Gallego Arias	2017-06-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was (once again) a spurious inter-dependency, that we solve by introducing a new module with the proper functionality. This helps in cleaning up the code. Note that no code was changed, other than removing the setting of the references.
* \| \|	[vernac] Remove unused hooks.	Emilio Jesus Gallego Arias	2017-06-20
\|/ / \| \| \| \| \| \|	These hooks are not used (leftovers?) and IMHO they should not be.
* \|	Clean up universes of constants and inductives	Amin Timany	2017-06-16
\| \|
* \|	Remove Warnings: unused value ...	Amin Timany	2017-06-16
\| \|
* \|	Change the option to Set Inductive Cumulativity	Amin Timany	2017-06-16
\| \| \| \| \| \| \| \| \| \|	This requires to change the status of Inductive (we have also changed CoInductive and Variant) from keyword to identifier.
* \|	Correct coqchk reduction	Amin Timany	2017-06-16
\| \|
* \|	Disable debug printing	Amin Timany	2017-06-16
\| \| \| \| \| \| \| \|	Fix a mistake in record declaration
* \|	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
\| \|