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`.
*	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.
* \|	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.
*	Remove fourier plugin	Maxime Dénès	2018-07-17
\| \| \| \|	As stated in the manual, the fourier tactic is subsumed by lra.
*	fixed typo for assert_suceed	charguer	2018-07-10
\|
*	Merge PR #8028: Fix a few typos	Théo Zimmermann	2018-07-10
\|\
\| *	Fix typo in doc/proof-engine/tactics.rst.	whitequark	2018-07-10
\| \|
* \|	Fix rst syntax for `quote ident {ident}`	Joachim Breitner	2018-07-09
\|/
*	hints: add Hint Variables/Constants Opaque/Transparent commands	Matthieu Sozeau	2018-07-02
\| \| \| \| \| \| \| \| \| \| \|	This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables
*	[ssr] document {}/view	Enrico Tassi	2018-06-22
\|
*	[ssr] document rewrite {}foo	Enrico Tassi	2018-06-22
\| \| \| \|	It was used in some examples, but never fully documented
*	Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter.	Maxime Dénès	2018-06-21
\|\
* \	Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.	Pierre-Marie Pédrot	2018-06-19
\|\ \
\| \| *	[doc] Fix a typo in the ssreflect chapter	Clément Pit-Claudel	2018-06-19
\| \| \|
\| \| *	[doc] Fix uncaught duplicate-label errors in the SSReflect chapter	Clément Pit-Claudel	2018-06-19
\| \|/ \|/\|
\| *	Fix #7421: constr_eq ignores universe constraints.	Gaëtan Gilbert	2018-06-18
\| \| \| \| \| \| \| \| \| \|	The test isn't quite the one in #7421 because that use of algebraic universes is wrong.
* \|	Fix #7829: Spurious documentation failures.	Théo Zimmermann	2018-06-18
\|/ \| \| \|	We split a Require Import in two to avoid reaching the timeout.
*	Improve links to SSR tactics, and some other improvements.	Théo Zimmermann	2018-06-05
\|
*	Workaround a weird error of .. coqtop::	Théo Zimmermann	2018-06-05
\|
*	Remove many abusive .. coqtop in SSR chapter.	Théo Zimmermann	2018-06-05
\| \| \| \|	Many still remain.
*	A few additional small fixes.	Théo Zimmermann	2018-06-05
\|
*	[sphinx] Fix missing indices warnings.	Théo Zimmermann	2018-06-05
\|
*	[ssr] index entry for "without loss", "suffices" and "generally have"	Enrico Tassi	2018-06-05
\|
*	[ssr] some fixes to the documentation markup	Enrico Tassi	2018-06-05
\|
*	[sphinx] Start fixing SSR chapter.	Théo Zimmermann	2018-06-05
\|
*	Merge PR #7229: Deprecate implicit tactic solving.	Hugo Herbelin	2018-06-04
\|\
* \	Merge PR #7601: Fix notation for code snippet in documentation	Maxime Dénès	2018-06-04
\|\ \
\| \| *	Documenting the deprecation.	Pierre-Marie Pédrot	2018-06-04
\| \|/ \|/\|
* \|	Merge PR #7648: Indicate in the doc that clearbody can take several idents	Maxime Dénès	2018-06-04
\|\ \
\| * \|	Merge two clearbody docs	Théo Winterhalter	2018-06-01
\| \| \|
\| * \|	Indicate in the doc that clearbody can take several idents	Théo Winterhalter	2018-05-31
\| \| \|
* \| \|	[doc] Allow more than one signature and name per Sphinx object	Clément Pit-Claudel	2018-05-25
\|/ / \| \| \| \| \| \|	As discussed in GH-7556.
\| *	Fix notation for code snippet in documentation	Anton Trunov	2018-05-25
\|/ \| \| \|	It failed to compile before because the type arguments were declared implicit after introducing the notation
*	Merge PR #7508: Improve rewrite section in tactic chapter.	Maxime Dénès	2018-05-25
\|\
* \|	Document nested proofs and associated option.	Théo Zimmermann	2018-05-17
\| \|
* \|	Merge PR #7517: [sphinx] Fix indentation at the end of proof handling chapter.	Maxime Dénès	2018-05-16
\|\ \
\| \| *	[sphinx] Fix mistake in index.	Théo Zimmermann	2018-05-16
\| \| \|
\| \| *	[sphinx] Improve rewrite section in tactic chapter.	Théo Zimmermann	2018-05-16
\| \|/ \|/\| \| \| \| \|	Including a fix to the example given in #7407.
* \|	[doc] Small fixes	Clément Pit-Claudel	2018-05-15
\| \|
\| *	[sphinx] Fix indentation at the end of proof handling chapter.	Théo Zimmermann	2018-05-15
\|/
*	Remove duplicate entries for Proof, Qed, Defined, Admitted.	Théo Zimmermann	2018-05-14
\| \| \| \|	And marginal improvements in the last section of the Gallina chapter.
*	Merge PR #7374: [sphinx] More fatal warnings.	Maxime Dénès	2018-05-14
\|\
* \|	Doc: Renaming an old-style numerical evar in an alphabetical one.	Hugo Herbelin	2018-05-11
\| \|
* \|	Doc: Moving `\forall` to `forall` in file tactics.rst.	Hugo Herbelin	2018-05-11
\| \| \| \| \| \| \| \| \| \|	Not only are most of "forall"s in the manual in Coq notation, but the math notation leads to have a specially long space after the comma.