coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Deprecate dead code option Congruence Depth.	Gaëtan Gilbert	2017-12-14
\|
*	Document Short Module Printing.	Gaëtan Gilbert	2017-12-14
\|
*	Document Rewriting Schemes (quickly).	Gaëtan Gilbert	2017-12-14
\|
*	Document Record Elimination Schemes.	Gaëtan Gilbert	2017-12-14
\|
*	Document Asymmetric Patterns.	Gaëtan Gilbert	2017-12-14
\|
*	Document some omega options (missing Omega Oldstyle).	Gaëtan Gilbert	2017-12-14
\|
*	Add doc for Set Debug RAKAM.	Gaëtan Gilbert	2017-12-14
\|
*	Add doc for Set Debug Cbv.	Gaëtan Gilbert	2017-12-14
\|
*	Add doc for Set Info/Debug Auto/Trivial/Eauto.	Gaëtan Gilbert	2017-12-14
\|
*	Add optindex for Set Bullet Behavior.	Gaëtan Gilbert	2017-12-14
\|
*	Add doc for Set Congruence Verbose	Gaëtan Gilbert	2017-12-14
\|
*	Fix typo in doc optindex for Typeclass Resolution ...	Gaëtan Gilbert	2017-12-14
\|
*	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.
* \ \ \ \ \	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	[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.
\| \| \| \| \| \| \| \| \| \| \| *	Register universe binders for record projections.	Gaëtan Gilbert	2017-11-24
\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| *	Stop exposing UState.universe_context and its Evd wrapper.	Gaëtan Gilbert	2017-11-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We can enforce properties through check_univ_decl, or get an arbitrary ordered context with UState.context / Evd.to_universe_context (the later being a new wrapper of the former).
\| \| \| \| \| \| \| \| \| \| \| *	Separate checking univ_decls and obtaining universe binder names.	Gaëtan Gilbert	2017-11-24
\| \| \| \| \| \| \| \| \| \| \| \|