coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[ci] Test coqchk on the CompCert target.	Théo Zimmermann	2017-11-30
\|
*	Merge PR #6269: [ci] [vst] Shorten compilation time to avoid Travis timeouts.	Maxime Dénès	2017-11-30
\|\
* \	Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as ↵	Maxime Dénès	2017-11-30
\|\ \ \| \| \| \| \| \| \| \| \|	instance.
* \ \	Merge PR #6271: Add PR backport script.	Maxime Dénès	2017-11-29
\|\ \ \
* \ \ \	Merge PR #6253: Fixing inconsistent associativity of level 10 in the table ↵	Maxime Dénès	2017-11-29
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	of levels
* \ \ \ \	Merge PR #6199: [vernac] Uniformize type of vernac interpretation.	Maxime Dénès	2017-11-29
\|\ \ \ \ \
\| \| \| * \| \|	Add PR backport script.	Théo Zimmermann	2017-11-28
\| \|_\|/ / / \|/\| \| \| \|
\| \| \| \| *	[ci] [vst] Shorten compilation time to avoid Travis timeouts.	Emilio Jesus Gallego Arias	2017-11-28
\| \|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove the progs target [examples] to save time, we still build the full library thou. I guess we can't do better for now unless we get some Travis subscription.
\| \| \| *	Fix (partial) #4878: option to stop autodeclaring axiom as instance.	Gaëtan Gilbert	2017-11-28
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6259: Add PR merge script.	Maxime Dénès	2017-11-28
\|\ \ \
\| * \| \|	Add PR merge script.	Maxime Dénès	2017-11-28
\| \| \| \|
* \| \| \|	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\ \ \ \
* \ \ \ \	Merge PR #6235: Fixing failing mkdir in test-suite for coq-makefile.	Maxime Dénès	2017-11-28
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6248: [api] Remove aliases of `Evar.t`	Maxime Dénès	2017-11-28
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6246: Ref. Man.: Updating the current official writing of OCaml; ↵	Maxime Dénès	2017-11-28
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	updating Camlp4->Camlp5.
\| \| \| \| \| \| * \|	[vernac] Adjust `interp` to pass polymorphic in the attributes.	Emilio Jesus Gallego Arias	2017-11-27
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	[vernac] Add polymorphic to the type of vernac interpration options.	Emilio Jesus Gallego Arias	2017-11-27
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	[vernac] Start to uniformize type of vernac interpretation.	Emilio Jesus Gallego Arias	2017-11-27
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In particular, we put all the context in the atts structure, and generalize the type of the parameters of a vernac. I hope this helps people working on "attributes", my motivation is indeed having a more robust interpretation.
* \| \| \| \| \| \|	Merge PR #6237: coq_makefile tests: build in easily removed temporary ↵	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|	subdirectory.
* \| \| \| \| \| \|	Merge PR #6242: Use Evarutil.has_undefined_evars for tactic has_evar.	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate.	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6207: [stm] Allow delayed constant in interactive mode.	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6238: Fix deprecated syntax warning from vernacextend.mlp.	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6241: [lib] Generalize Control.timeout type.	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6228: Make byte on gitlab.	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6226: Enhance votour	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6149: Update TimeFileMaker.py to correctly sort timing diffs	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6041: Protecting the printing of filenames with space	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6227: Linter: do not lint untracked files.	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	A cosmetic standardization: adding a space in g_constr.ml4.	Hugo Herbelin	2017-11-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Releasing level "11" of "pattern".	Hugo Herbelin	2017-11-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was introduced in 0917ce7c to fix #4272, but it seems that we can fix it by just merging levels 10 and 11. This prevents the worry of fixing the associativity of level 11 to left in 0917ce7c.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Fixing associativity registered for level 10.	Hugo Herbelin	2017-11-27
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Apparently a long-standing bug, coupled with a pattern/constr associativity inconsistency introduced while fixing another pattern/constr level inconsistency (bug #4272, 0917ce7c).
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	There don't really bring anything, we also correct some minor nits with the printing function.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Overlay for stronger restrict_universe_context.	Gaëtan Gilbert	2017-11-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Restrict universe context when declaring constants in obligations.	Gaëtan Gilbert	2017-11-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Updating the current official writing of OCaml, updating Camlp4->Camlp5.	Hugo Herbelin	2017-11-25
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| *	Fix #5347: unify declaration of axioms with and without bound univs.	Gaëtan Gilbert	2017-11-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Note that this makes the following syntax valid: Axiom foo@{i} bar : Type@{i}. (ie putting a universe declaration on the first axiom in the list, the declaration then holds for the whole list).
\| \| \| \| \| \| \| \| \| \| \| \| \| *	Fix interpretation of global universes in univdecl constraints.	Gaëtan Gilbert	2017-11-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Also nicer error when the constraints are impossible.
\| \| \| \| \| \| \| \| \| \| \| \| \| *	Forbid repeated names in universe binders.	Gaëtan Gilbert	2017-11-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| *	Universe binders survive sections, modules and compilation.	Gaëtan Gilbert	2017-11-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| *	Allow local universe renaming in Print.	Gaëtan Gilbert	2017-11-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| *	Make restrict_universe_context stronger.	Gaëtan Gilbert	2017-11-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This fixes BZ#5717. Also add a test and fix a changed test.
\| \| \| \| \| \| \| \| \| \| \| \| \| *	Fix obligations handling of universes anticipating stronger restrict	Matthieu Sozeau	2017-11-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \|	[lib] Generalize Control.timeout type.	Emilio Jesus Gallego Arias	2017-11-24
\| \|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We also remove some internal implementation details from the mli file, there due historical reasons.
\| \| \| \| \| \| \| \| \| * \| \| \|	Use Evarutil.has_undefined_evars for tactic has_evar.	Gaëtan Gilbert	2017-11-24
\| \|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| *	In close_proof only check univ decls with the restricted context.	Gaëtan Gilbert	2017-11-24
\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| *	Use Entries.constant_universes_entry more.	Gaëtan Gilbert	2017-11-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reduces conversions between ContextSet/UContext and encodes whether we are polymorphic by which constructor we use rather than using some boolean.
\| \| \| \| \| \| \| \| \| \| \| *	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Also use constant_universes_entry instead of a bool flag to indicate polymorphism in ParameterEntry. There are a few places where we convert back to ContextSet because check_univ_decl returns a UContext, this could be improved.
\| \| \| \| \| \| \| \| \| \| \| *	restrict_universe_context: do not prune named universes.	Gaëtan Gilbert	2017-11-24
\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| *	Fix defining non primitive projections with abstracted universes.	Gaëtan Gilbert	2017-11-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	I think this only affects printing (in the new test you would get [Var (0)] when printing runwrap) but is still ugly.