coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-04-02	Remove the omega tactic and related options	Jim Fehrle

2021-03-08	Convert 2nd part of rewriting chapter to prodn	Jim Fehrle

2020-12-30	Convert rewriting and proof-mode chapters to prodn	Jim Fehrle

2020-11-09	[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.	Théo Zimmermann
	The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version.
2020-11-05	Change the title of the automatic tactic chapter and of its sections.	Théo Zimmermann
	Prefer the term 'solver' to 'decision procedure'.
2020-10-20	Add some missing smallcaps.	Théo Zimmermann

2020-04-20	[refman] Remove references to omega from Tactics chapter.	Théo Zimmermann
	Omega was defined twice and this is the tactics chapter documentation which was refered to from the tactic index. We remove it so that users find the other reference (which contains the deprecation notice). The changes to the doc of zarith are a follow-up to #11976.
2020-04-17	Deprecate “omega”	Vincent Laporte

2020-01-08	[refman] [changelog] Announce omega replacement.	Théo Zimmermann

2019-11-06	Replace "option" in doc when it refers to a flag	Jim Fehrle

2018-11-21	[sphinx] Progress towards closing #7602: remove most objects without a body.	Théo Zimmermann
	Remove objects without body from most chapters. The remaining problems are all in the SSReflect chapter.
2018-09-25	Remove romega	Vincent Laporte

2018-09-20	Rewrite "Flags, Options and Tables" section.	Jim Fehrle
	Mark boolean-valued options with :flag: Adjust tactic and command names so parameters aren't shown in the index unless they're needed for disambiguation. Remove references to synchronous options. Revise doc for tables. Correct indentation for text below :flag:
2018-09-10	Deprecate romega in favor of lia.	Vincent Laporte

2018-08-31	Uniformized many spelling variants. Added .. warning:: and .. seealso:: ↵	Zeimer
	directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
2018-08-01	Improved grammar and spelling in chapters 'Type Classes', 'Omega' and ↵	Zeimer
	'Micromega' of the Reference Manual.
2018-05-09	[sphinx] Fix new warnings related to tacn, cmd, opt...	Théo Zimmermann

2018-05-05	[sphinx] Re-indent to get much better rendering.	Théo Zimmermann
	Add some more cmd references. And use deprecated directives.
2018-05-05	Add some refs in the Omega chapter.	Théo Zimmermann

2018-05-05	Fix error messages and make them consistent.	Théo Zimmermann
	All the error messages start with a capitalized letter and end with a dot.
2018-03-22	[Sphinx] Add chapter 21	Maxime Dénès
	Thanks to Pierre Letouzey for porting this chapter.
2018-03-22	[Sphinx] Move chapter 21 to new infrastructure	Maxime Dénès