coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
* \| \| \| \| \| \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6187: Check findlib version in configure (fix #4270).	Maxime Dénès	2017-11-23
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag.	Maxime Dénès	2017-11-23
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| * \| \| \|	[plugin] Remove LocalityFixme über hack.	Emilio Jesus Gallego Arias	2017-11-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	To that extent we introduce a new prototype vernacular extension macro `VERNAC COMMAND FUNCTIONAL EXTEND` that will take a function with the proper parameters and attributes. This of course needs more refinement, in particular we should move `vernac_command` to its own file and make `Vernacentries` consistent wrt it.
\| \| \| \| \| \| \| \| \| \| * \| \| \|	[plugin] Encapsulate modifiers to vernac commands.	Emilio Jesus Gallego Arias	2017-11-22
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is a continuation on #6183 and another step towards a more functional interpretation of commands. In particular, this should allow us to remove the locality hack.
\| \| \| \| \| \| \| \| \| \| * \| \|	Add test-suite tests for timing scripts	Jason Gross	2017-11-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	These work on precomputed build logs (in this case, from a recent partial build of fiat-crypto). They are meant to serve as human-readable sanity checks of output format. Separate out the sane bits of template/init.sh from the ones messing with directory structure (which are fragile and make assumptions about where the calling script is sourcing it from). N.B. The test-suite removes all .log files, so we use .log.in. N.B. We set COQLIB in precomputed-time-tests/run.sh, not the Makefile, because coqc, on Windows, doesn't handle cygwin paths passed via -coqlib, and `pwd` gives cygwin paths. N.B. We have .gitattributes to satisfy the linter (as per https://github.com/coq/coq/pull/6149#issuecomment-346410990)
\| \| \| \| \| \| \| \| \| \| * \| \|	Update TimeFileMaker.py to correctly sort timing diffs	Jason Gross	2017-11-22
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Previously, it was reverse-ordering timing diffs.
\| \| \| \| \| \| \| \| \| \| * \|	Implement a tail-recursive traversal of the object in votour.	Pierre-Marie Pédrot	2017-11-22
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \| \|	[api] A few more minor deprecation notices.	Emilio Jesus Gallego Arias	2017-11-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Note the problem with `create_evar_defs`.
\| \| \| \| \| \| \| * \| \| \|	[api] Re-enable deprecation warnings.	Emilio Jesus Gallego Arias	2017-11-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	With a bit of care we can enable full deprecation warnings again in this funny file.
\| \| \| \| \| \| \| * \| \| \|	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`.
\| \| \| \| \| \| \| \| * \| \|	Fix universe polymorphic Program obligations.	Matthieu Sozeau	2017-11-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The universes of the obligations should all be non-algebraic as they might appear in instances of other obligations and instances only take non-algebraic universes as arguments.
\| \| \| \| \| \| \| * \| \| \|	[api] Miscellaneous consolidation + moves to engine.	Emilio Jesus Gallego Arias	2017-11-21
\| \|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We deprecate a few functions that were deprecated in the comments plus we place `Nameops` and `Univops` in engine where they do seem to belong in the large picture of code organization.
* \| \| \| \| \| \| \| \| \|	Merge PR #6173: [printing] Deprecate all printing functions accessing the ↵	Maxime Dénès	2017-11-21
\|\ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	global proof.
\| \| \| \| \| \| * \| \| \| \|	[stm] [doc] Add some documentation to AsyncTaskQueue API	Emilio Jesus Gallego Arias	2017-11-21
\| \|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	As a bonus we remove some trailing whitespace, and implement a couple of hints suggested in the discussion.
\| * \| \| \| \| \| \| \| \|	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
\|/ / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We'd like to handle proofs functionally we thus recommend not to use printing functions without an explicit context. We also adapt most of the code, making more explicit where the printing environment is coming from. An open task is to refactor some code so we gradually make the `Pfedit.get_current_context ()` disappear.
* \| \| \| \| \| \| \| \|	Merge PR #6185: [parser] Remove unnecessary statically initialized hook.	Maxime Dénès	2017-11-21
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6181: [proof] Attempt to deprecate some V82 parts of the proof API.	Maxime Dénès	2017-11-21
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6178: Have the coq_makefile timing test-suite print more	Maxime Dénès	2017-11-21
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| *	[stm] Allow delayed constant in interactive mode.	Emilio Jesus Gallego Arias	2017-11-21
\| \| \| \| \| \| \| \| \| \| \|/ \| \| \| \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This setting is a debug assertion, due to the many flags we still over-approximate setting the flag to true to all interactive environments. [So the assert is checked in vo compilation] Fixes #6152.
* \| \| \| \| \| \| \| \| \| \|	Merge PR #6168: Add Equations to CI	Maxime Dénès	2017-11-21
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6113: Extra work on ltac printing: fixing #5787, some parentheses	Maxime Dénès	2017-11-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	Fixes #5787 (printing of "constr:" lost in the move of constr to Generic).	Hugo Herbelin	2017-11-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Was broken since 8.6.
\| \| \| \| \| \| \| \| \| \| \| *	Fixing factorization of recursive notations in the case of an atomic separator.	Hugo Herbelin	2017-11-20
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This addresses a limitation found in math-comp seq.v file. See the example in test suite file success/Notations2.v. To go further and accept recursive notations with a separator made of several tokens, and assuming camlp5 unchanged, one would need to declare an auxiliary entry for this sequence of tokens and use it as an "atomic" (non-terminal) separator. See PR #6167 for details.
\| \| \| \| \| \| \| \| \| \| *	Remove pidentref grammar entry.	Gaëtan Gilbert	2017-11-20
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Replaced by ident_decl in #688.