coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Correct some spelling errorsmaster	Benjamin Barenblat	2018-07-22
\| \| \| \| \| \| \| \| \| \|	Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`.
*	Merge PR #8095: Improvements for the chapter 'Detailed examples of tactics' ↵	Théo Zimmermann	2018-07-22
\|\ \| \| \| \| \| \|	of the Reference Manual.
\| *	Solved problems with snippets giving errors in chapter 'Detailed examples of ↵	Zeimer	2018-07-21
\| \| \| \| \| \| \| \|	tactics' of the Reference Manual. Refreshed the section on the cardinality of the naturals. Removed the mention of specialize_eqs as it seems very bugged.
\| *	Rewrote examples about permutations, logic and type isomorphisms: changed ↵	Zeimer	2018-07-21
\| \| \| \| \| \| \| \|	the formatting and renamed the tactics to match modern naming conventions.
\| *	Improvements for the chapter 'Detailed examples of tactics' of the Reference ↵	Zeimer	2018-07-21
\|/ \| \| \|	Manual.
*	Merge PR #8072: Fixes for chapters 'Vernacular commands', 'Proof handling' ↵	Théo Zimmermann	2018-07-21
\|\ \| \| \| \| \| \|	and 'Tactics' of the Reference Manual.
* \	Merge PR #8086: Improved chapter 'The tactic language' of the Reference Manual.	Théo Zimmermann	2018-07-21
\|\ \
\| * \|	Small improvements suggested in comments to PR #8086.	Zeimer	2018-07-20
\| \| \|
\| * \|	Improved chapter 'The tactic language' of the Reference Manual.	Zeimer	2018-07-20
\|/ /
\| *	Added :undocumented: and :cmd: as suggested in comments for PR #8072.	Zeimer	2018-07-20
\| \|
\| *	Fixed many spelling and grammar errors in the chapters 'Vernacular ↵	Zeimer	2018-07-20
\|/ \| \| \| \| \| \|	commands', 'Proof handling' and 'Tactics' of the Reference Manual. Fixed some more serious errors related to tactics functional induction, unfold, hnf and red. Added some error messages and remarks for tactics btauto, rtauto and red.
*	Merge PR #8037: Export a function to apply toplevel tactic values in Tacinterp.	Enrico Tassi	2018-07-20
\|\
* \	Merge PR #8089: Remove declare_object for SsrHave NoTCResolution.	Enrico Tassi	2018-07-20
\|\ \
* \ \	Merge PR #8070: Fixed some typos and grammar errors from section 'The ↵	Théo Zimmermann	2018-07-20
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	language' of the Reference Manual.
\| * \| \|	Rewrote section 'Accessing the Type level' in the chapter 'The Coq library' ↵	Zeimer	2018-07-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	of the Reference Manual.
\| * \| \|	Fixed some typos and grammar errors from section 'The language' of the ↵	Zeimer	2018-07-19
\|/ / / \| \| \| \| \| \| \| \| \|	Reference Manual. Removed all mentions of prodT because it is no longer a separate inductive definition (prod has been living in Type for some time) but rather only a notation for prod needed for compatibility purposes.
* \| \|	Merge PR #7941: Extend QuestionMark to produce a better error message in ↵	Pierre-Marie Pédrot	2018-07-19
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	case of missing record field
\| \| * \|	Remove declare_object for SsrHave NoTCResolution.	Maxime Dénès	2018-07-19
\| \|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	IIUC, this was a hack to make `Set SsrHave NoTCResolution` behave like `Global Set SsrHave NoTCResolution`. I don't think it is needed (just let the user write the desired locality), but if it is, the right way of doing it is to let clients of Goptions specify a default locality.
* \| \|	Merge PR #8054: [dev] Autogenerate OCaml dev files.	Enrico Tassi	2018-07-18
\|\ \ \
* \ \ \	Merge PR #7897: Remove fourier plugin	Enrico Tassi	2018-07-18
\|\ \ \ \
* \ \ \ \	Merge PR #8068: [build] Build Coq and plugins with `-strict-sequence`	Enrico Tassi	2018-07-18
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #8060: Remove useless libobject in proof_using	Enrico Tassi	2018-07-18
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #8055: Fast accumulator check in native compilation	Maxime Dénès	2018-07-17
\|\ \ \ \ \ \ \
\| \| \| \| * \| \| \|	Remove fourier plugin	Maxime Dénès	2018-07-17
\| \|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	As stated in the manual, the fourier tactic is subsumed by lra.
\| \| \| \| \| * \|	change into QuestionMark default	Siddharth Bhat	2018-07-17
\| \| \| \| \| \| \|
\| \| \| \| \| * \|	Add overlay for Coq-Equations for QuestionMark.	Siddharth Bhat	2018-07-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The changed QuestionMark structure breaks Coq-Equations. Add an overlay to fix this.
\| \| \| \| \| * \|	Change QuestionMark for better record field missing error message.	Siddharth Bhat	2018-07-17
\| \|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	While we were adding a new field into `QuestionMark`, we decided to go ahead and refactor the constructor to hold an actual record. This record now holds the name, obligations, and whether the evar represents a missing record field. This is used to provide better error messages on missing record fields.
* \| \| \| \| \|	Merge PR #8069: Only check overlay extensions on git-tracked files	Gaëtan Gilbert	2018-07-16
\|\ \ \ \ \ \
\| * \| \| \| \| \|	Only check overlay extensions on git-tracked files	Jason Gross	2018-07-16
\|/ / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This way, when editors leave over temporary files from editing user-overlays, we don't prevent commits unless they are added to git.
* \| \| \| \| \|	Merge PR #8023: Introduce a team of code owners for the CI system.	Maxime Dénès	2018-07-16
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #8066: [ltac] Remove unused functions.	Pierre-Marie Pédrot	2018-07-16
\|\ \ \ \ \ \ \
\| \| \| \| \| * \| \|	[build] Build Coq and plugins with `-strict-sequence`	Emilio Jesus Gallego Arias	2018-07-14
\| \|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes #8067. This is becoming the default in many developments, so it makes sense to require it too, both for Coq and for Plugins.
\| * \| \| \| \| \|	[ltac] Remove unused functions / constructors.	Emilio Jesus Gallego Arias	2018-07-14
\|/ / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Catched by compiling the ml files from ml4.
* \| \| \| \| \|	Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of ↵	Théo Zimmermann	2018-07-13
\|\ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	the Reference Manual (Introduction, Credits).
\| \| \| \| * \| \|	Remove useless libobject in proof_using	Maxime Dénès	2018-07-13
\| \| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #6930: Make -warn-error fail on warnings emitted by coqc on stdlib.	Emilio Jesus Gallego Arias	2018-07-13
\|\ \ \ \ \ \ \
\| * \| \| \| \| \| \|	Make -warn-error fail on warnings emitted by coqc on stdlib.	Maxime Dénès	2018-07-13
\|/ / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We turn all Coq warnings that are on by default into errors.
\| \| \| * \| \| \|	Generate type-specific code for is_accu in native compilation of fixpoints.	Pierre-Marie Pédrot	2018-07-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is much more efficient than using Nativevalues.is_accu function which incurs a lot of irrelevant checks on its argument.
\| \| \| * \| \| \|	Store the {struct} inductive type in native fixpoint AST.	Pierre-Marie Pédrot	2018-07-13
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Pass a proper environment to Nativelambda.lambda_of_constr.	Pierre-Marie Pédrot	2018-07-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	No need to roll up a new data structure when Environment has O(log n) add and lookup of rel definitions.
\| * \| \| \| \| \|	Fixed typos, wording and grammar errors in the Preamble of the Reference ↵	Zeimer	2018-07-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Manual (Introduction, Credits).
* \| \| \| \| \| \|	Merge PR #8041: [ci] Remove warning jobs in favor of default `-warn-error yes`	Gaëtan Gilbert	2018-07-12
\|\ \ \ \ \ \ \ \| \|_\|_\|/ / / / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #7907: Tactic deprecation machinery	Pierre-Marie Pédrot	2018-07-12
\|\ \ \ \ \ \ \ \| \|_\|/ / / / / \|/\| \| \| \| \| \|
\| \| \| \| \| * \|	[dev] Autogenerate OCaml dev files.	Emilio Jesus Gallego Arias	2018-07-12
\| \|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	For now we only copy the templates, but we could do more fancy stuff. This helps to be compatible with build systems that take care of these files automatically, see: https://github.com/coq/coq/pull/6857#discussion_r202096579
* \| \| \| \| \|	Merge PR #8051: Clean-up user-overlays folder.	Emilio Jesus Gallego Arias	2018-07-12
\|\ \ \ \ \ \
\| * \| \| \| \| \|	Clean-up user-overlays folder.	Théo Zimmermann	2018-07-12
\| \| \|_\|_\|/ / \| \|/\| \| \| \|
\| \| \| * \| \|	[warnings] Disable warning 58 "no cmx file was found in path"	Emilio Jesus Gallego Arias	2018-07-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	See https://github.com/ocaml/num/issues/9
\| \| \| * \| \|	[warnings] Disable warning 59 [assignment to a non-mutable value] to make ↵	Emilio Jesus Gallego Arias	2018-07-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	flambda happy. See issue #8043. Using `[@@@ocaml.warning "-59"]` to disable this fails, it seems like an OCaml bug.
\| \| \| * \| \|	[ci] Remove warning jobs in favor of default `-warn-error yes`	Emilio Jesus Gallego Arias	2018-07-12
\| \|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	As discussed in #6930, we remove the warnings jobs and instead do require the developers to submit a clean build.
* \| \| \| \|	Merge PR #7871: [ci] Upgrade edge OCaml to 4.07.0 and Dune to 1.0.0	Gaëtan Gilbert	2018-07-12
\|\ \ \ \ \ \| \|/ / / / \|/\| \| \| \|