coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[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
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \|	[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
\| \|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \|	Merge PR #6231: Fix link to Recursive Make Considered Harmful	Maxime Dénès	2017-11-24
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRing	Maxime Dénès	2017-11-24
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #486: Make some functions on terms more robust w.r.t new term ↵	Maxime Dénès	2017-11-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	constructs.
\| \| \| \| \| \| \| \| \| * \| \| \|	Fix deprecated syntax warning from vernacextend.mlp.	Gaëtan Gilbert	2017-11-24
\| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion	Maxime Dénès	2017-11-24
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| *	coq_makefile tests: build in easily removed temporary subdirectory.	Gaëtan Gilbert	2017-11-24
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This allows us to avoid doing git clean.
\| \| \| \| \| \| \| \| \| \| \| *	Fix coq-makefile ocamldoc call when configured with -annotate.	Gaëtan Gilbert	2017-11-24
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes #6120.
\| \| \| \| \| \| \| \| \| * \|	Make byte on gitlab.	Gaëtan Gilbert	2017-11-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Hopefully this will stop the intermittent test-suite/coq-makefile/findlib-package failures.
* \| \| \| \| \| \| \| \| \| \|	Update PR filter used by RM.	Maxime Dénès	2017-11-24
\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #6197: [plugin] Remove LocalityFixme über hack.	Maxime Dénès	2017-11-24
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \| \|	Unify style of comments in file CUnix.	Hugo Herbelin	2017-11-23
\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \|	Quote file names which have spaces in "Print LoadPath".	Hugo Herbelin	2017-11-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The primary concern is for clarity of reading. May it affects tools which would parse the output of "Print LoadPath"? Presumably, these tools would not support file names with spaces already, so this may have no impact.
\| \| \| \| \| \| \| * \| \| \| \|	Add a function to surround filenames containing a space with quotes.	Hugo Herbelin	2017-11-23
\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \| \|	Surrounding a few places printing file names with quotes when a space occurs.	Hugo Herbelin	2017-11-23
\| \|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \|	Make one more function robust in term_dnet.ml	Maxime Dénès	2017-11-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was actually forgotten in native-coq.
\| \| \| * \| \| \| \| \| \| \|	Make some functions on terms more robust w.r.t new term constructs.	Maxime Dénès	2017-11-23
\| \| \| \| \|_\|_\|_\|_\|/ / \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Extending terms is notoriously difficult. We try to get more help from the compiler by making sure such an extension will trigger non exhaustive pattern matching warnings.
* \| \| \| \| \| \| \| \| \|	Merge PR #6167: Fixing factorization of recursive notations with an atomic ↵	Maxime Dénès	2017-11-23
\|\ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	separator
* \ \ \ \ \ \ \ \ \ \	Merge PR #6203: Fix universe polymorphic Program obligations.	Maxime Dénès	2017-11-23
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6186: [api] Miscellaneous consolidation.	Maxime Dénès	2017-11-23
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6221: Add PR filter used by RM to the contributing guide.	Maxime Dénès	2017-11-23
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \|	Fix link to Recursive Make Considered Harmful	Gaëtan Gilbert	2017-11-23
\| \|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	Add PR filter used by RM to the contributing guide.	Maxime Dénès	2017-11-23
\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \|	Linter: do not lint untracked files.	Gaëtan Gilbert	2017-11-23
\| \|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \|	Adding ad hoc overlay for sf/vfa.	Hugo Herbelin	2017-11-23
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \|	Recognizing Z in romega up to conversion.	Hugo Herbelin	2017-11-23
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \|	Using is_conv rather than eq_constr to find `nat` or `Z` in omega.	Hugo Herbelin	2017-11-23
\| \|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Moving at the same to a passing "env sigma" style rather than passing "gl". Not that it is strictly necessary, but since we had to move functions taking only a "sigma" to functions taking also a "env", we eventually adopted the "env sigma" style. (The "gl" style would have been as good.) This answers wish #4717.
\| \| \| \| \| \| * \| \| \|	Fixing a 8.7 regression of ring_simplify in ArithRing.	Hugo Herbelin	2017-11-23
\| \|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	With help from Guillaume (see discussion at https://github.com/coq/coq/issues/6191).
\| \| \| \| \| \| \| * \|	Truncate strings in votour to 1024 characters.	Pierre-Marie Pédrot	2017-11-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Making it bigger is kind of useless, takes time and clutters the output for no real advantage.
* \| \| \| \| \| \| \| \|	Merge PR #6200: Remove pidentref grammar entry.	Maxime Dénès	2017-11-23
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #1092: [stm] [doc] Add some documentation to obscure AsyncTaskQueue	Maxime Dénès	2017-11-23
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \|	Bypass int and string representation in votour when it's incorrect.	Pierre-Marie Pédrot	2017-11-23
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \|	Tail-recursive list traversal in votour.	Pierre-Marie Pédrot	2017-11-23
\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #6123: Nix file	Maxime Dénès	2017-11-23
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6189: Disable whitespace linter for .out files.	Maxime Dénès	2017-11-23
\|\ \ \ \ \ \ \ \ \ \ \ \