coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR #7679: Clean native compilation of primitive projections	Maxime Dénès	2018-06-05
\|\
* \	Merge PR #7004: Make `simple apply` obey `Opaque` directive.	Pierre-Marie Pédrot	2018-06-05
\|\ \
* \ \	Merge PR #7077: Preserving canonical structure of return predicate in ↵	Maxime Dénès	2018-06-05
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	vm_compute and native_compute (partial fix to #7068; also fixes #7076))
* \ \ \	Merge PR #7663: test suite: make target to regenerate failing output tests	Enrico Tassi	2018-06-05
\|\ \ \ \
* \ \ \ \	Merge PR #7464: Make whitespace linter not check for trailing space.	Maxime Dénès	2018-06-05
\|\ \ \ \ \
\| \| \| \| \| *	More straightforward native compilation of primitive projections.	Pierre-Marie Pédrot	2018-06-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Instead of having a constant-based compilation of projections, we generate them at the compilation time of the inductive block to which they pertain.
\| \| \| \| \| *	Use projection indices in native compilation rather than constant names.	Pierre-Marie Pédrot	2018-06-05
\| \|_\|_\|_\|/ \|/\| \| \| \|
* \| \| \| \|	Merge PR #7643: Fix #7631: native_compute fails to compile an example in Coq 8.8	Pierre-Marie Pédrot	2018-06-05
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7690: Fixing typos in file Berardi.v	Pierre-Marie Pédrot	2018-06-05
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7646: Fix #4714: Stack overflow with native compute	Pierre-Marie Pédrot	2018-06-05
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7099: Stronger invariants in unification signature.	Matthieu Sozeau	2018-06-05
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7453: Refuse to parse empty [Context] command.	Matthieu Sozeau	2018-06-05
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #7495: Fix restrict_universe_context	Matthieu Sozeau	2018-06-05
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| *	Make direct invocations of `simple apply` obey `Opaque` directive.	Maxime Dénès	2018-06-05
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	When called by auto, `simple apply` still does not respect `Opaque` because of compatibility issues.
\| \| \| \| \| \| * \| \| \|	Fix #7631: native_compute fails to compile an example in Coq 8.8	Maxime Dénès	2018-06-04
\| \|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Dependency analysis for separate compilation was not iterated properly on rel_context and named_context.
* \| \| \| \| \| \| \| \|	Merge PR #7315: An attempt to clarify error message for Arguments needing ↵	Maxime Dénès	2018-06-04
\|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	"rename" flag
\| \| \| \| \| \| \| \| \| *	Tests for part of #7068 and for #7076 (vm/native_compute and return predicate).	Hugo Herbelin	2018-06-04
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| *	Preserving "canonical" form of return predicate in native_compute.	Hugo Herbelin	2018-06-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Note that the normalization of the context of the return predicate was not done by the native compilation but by the lazy machine. The patch also "fixes" an anomaly in the case of an arity which was not in canonical form as in: Inductive A : nat -> id (nat->Type) := . Eval native_compute in fun x => match x in A y z return y = z with end.
\| \| \| \| \| \| \| \| \| *	Preserving "canonical" form of return predicate in vm_compute.	Hugo Herbelin	2018-06-04
\| \|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Note that the normalization of the context of the return predicate was not done by the vm but by the lazy machine. The patch also "fixes" an anomaly in the case of an arity which was not in canonical form as in: Inductive A : nat -> id (nat->Type) := . Eval vm_compute in fun x => match x in A y z return y = z with end.
* \| \| \| \| \| \| \| \|	Merge PR #7229: Deprecate implicit tactic solving.	Hugo Herbelin	2018-06-04
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #7486: Update old parts of CHANGES to use current bug numbers.	Hugo Herbelin	2018-06-04
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #7481: document 7025 (coq_makefile flag variables)	Maxime Dénès	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #7596: [ci] [windows] Use newer OCaml version.	Michael Soegtrop	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-	Pierre-Marie Pédrot	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| * \|	Make whitespace linter not check for trailing newlines.	Gaëtan Gilbert	2018-06-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	git does not know how to fix this automatically when they appear by removing a chunk of text at the end of the file. eg ``` foo bar ``` to ``` foo ```
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7601: Fix notation for code snippet in documentation	Maxime Dénès	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7418: Actually take advantage of the normalization status of ↵	Maxime Dénès	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	kernel closures.
\| \| \| \| \| \| \| \| \| \| \| \| \| \| *	test suite: make target to regenerate failing output tests	Gaëtan Gilbert	2018-06-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7199: Fixes #7195: missing freshness condition in Ltac ↵	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	pattern-matching names
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7112: Fix #6770: fixpoint loses locality info in proof mode.	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7114: Fix #7113: Program Let Fixpoint in section causes anomaly	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7189: Fix #5539: algebraic universe produced by cases.	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7349: Fix an anomaly when calling Obligation 0 or Obligation -1.	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Documenting the API change.	Pierre-Marie Pédrot	2018-06-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Adding an overlay for the Equations plugin.	Pierre-Marie Pédrot	2018-06-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Stronger invariants in unification signature.	Pierre-Marie Pédrot	2018-06-04
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We use an option type instead of returning a pair with a boolean. Indeed, the boolean being true was always indicating that the returned value was unchanged. The previous API was somewhat error-prone, and I don't understand why it was designed this way in the first place.
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7013: Fixes #7011: Fix/CoFix were not considered in main loop of ↵	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	tactic unification.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7216: Replace uses of Termops.dependent by more specific functions.	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7552: Fix #7539: Checker does not properly handle negative ↵	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	coinductive types.
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7590: Fix #7586: Anomaly "Uncaught exception Not_found".	Matthieu Sozeau	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Documenting the deprecation.	Pierre-Marie Pédrot	2018-06-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Deprecate implicit tactic solving.	Pierre-Marie Pédrot	2018-06-04
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7249: Cleaning, documentation, uniformisation of the Coq extension ↵	Pierre-Marie Pédrot	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	of List
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7619: Mention test-suite in PR template	Maxime Dénès	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7648: Indicate in the doc that clearbody can take several idents	Maxime Dénès	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.	Maxime Dénès	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7657: Fix a couple typos in deprecation messages	Pierre-Marie Pédrot	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7640: Small refactoring to clarify make_local_hint_db.	Pierre-Marie Pédrot	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7649: Remove some dead code in class_tactics.ml	Pierre-Marie Pédrot	2018-06-04
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Fixing typos in file Berardi.v	Hugo Herbelin	2018-06-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Note that one of them is in the name of the main theorem, so we use a compatibility notation.