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`.
*	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.
*	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
*	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.
*	A few additional small fixes.	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 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
\| \|
\| *	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
*	[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
\|
*	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.
* \|	Doc: Some quotes missing in file tactics.rst.	Hugo Herbelin	2018-05-11
\| \|
* \|	Replacing a broken reference by hyperlinks in chapter tactics.	Hugo Herbelin	2018-05-11
\| \|
* \|	A few fixes in chapter tactics.	Hugo Herbelin	2018-05-11
\| \|
\| *	[sphinx] Fix new warnings related to tacn, cmd, opt...	Théo Zimmermann	2018-05-09
\| \|
\| *	Replacing a broken reference by hyperlinks in chapter tactics.	Hugo Herbelin	2018-05-09
\| \|
\| *	A few fixes in chapter tactics.	Hugo Herbelin	2018-05-09
\|/
*	[sphinx] Fixes around apply, including indentation and fixing a Coq warning.	Théo Zimmermann	2018-05-05
\|
*	[sphinx] Fixes around refine, including indentation and a hard-coded ref.	Théo Zimmermann	2018-05-05
\|
*	[sphinx] Improvements around injection tactic.	Théo Zimmermann	2018-05-05
\|
*	[sphinx] Improve part about Hints.	Théo Zimmermann	2018-05-05
\| \| \| \|	Fix Hint (Transparent \| Opaque) index.
*	Clean-up around cmd documentation.	Théo Zimmermann	2018-05-05
\| \| \| \|	In particular, remove trailing dots.
*	[sphinx] More reference fixes.	Théo Zimmermann	2018-05-05
\|
*	Fix error messages and make them consistent.	Théo Zimmermann	2018-05-05
\| \| \| \|	All the error messages start with a capitalized letter and end with a dot.
*	Add direct reference to congruence with.	Théo Zimmermann	2018-05-05
\|
*	Clean-up around options.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \|	- Remove all trailing dots. - There is only one Bullet Behavior option. - Replaces `@natural` and `@integer` by `@num`.
*	debug trivial and debug auto were not in the tactic index.	Théo Zimmermann	2018-05-05
\|
*	[sphinx] Backport reformulation.	Théo Zimmermann	2018-05-05
\| \| \| \|	(cf. 711b9d8cdf6e25690d247d9e8c49f005527e64e2)
*	Make "intro"/"intros" progress on existential variables.	Hugo Herbelin	2018-05-02
\|
*	Strict focusing using Default Goal Selector.	Gaëtan Gilbert	2018-04-29
\| \| \| \| \| \| \| \| \| \| \| \|	We add a [SelectAlreadyFocused] constructor to [goal_selector] (read "!") which causes a failure when there's not exactly 1 goal and otherwise is a noop. Then [Set Default Goal Selector "!".] puts us in "strict focusing" mode where we can only run tactics if we have only one goal or use a selector. Closes #6689.
*	[Sphinx] Clean-up indices	Maxime Dénès	2018-04-16
\|
*	[Sphinx] Fix a lot of references and description of options	Maxime Dénès	2018-04-16
\|
*	[Sphinx] Fix all remaining warnings.	Maxime Dénès	2018-04-14
\|
*	[sphinx] Fix many warnings.	Théo Zimmermann	2018-04-14
\| \| \| \| \|	Including cross-reference TODOs. I took down the number of warnings from 300 to 50.
*	Clarify wording in tactics documentation.	Théo Zimmermann	2018-03-25
\| \| \| \|	Closes #6980.
*	[Sphinx] Add chapter 8	Maxime Dénès	2018-03-15
\| \| \| \|	Thanks to Heiko Becker and Nikita Zyuzin for porting this chapter.
*	[Sphinx] Move chapter 8 to new infrastructure	Maxime Dénès	2018-03-15