coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-11-14	Distinguish one_pattern and one_term nonterminals	Jim Fehrle

2020-11-12	Merge PR #13345: Addressing #13344: clarifying the role of Add ML Path vs -I	coqbot-app[bot]
	Reviewed-by: ejgallego Reviewed-by: Zimmi48 Ack-by: ppedrot Ack-by: jfehrle
2020-11-12	Clarifying the role of Add ML Path vs -I (see #13344).	Hugo Herbelin
	Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-11-12	Merge PR #13317: [ssr] intro pattern extensions for dup, swap and apply	coqbot-app[bot]
	Reviewed-by: gares Ack-by: Zimmi48
2020-11-10	Convert logic.rst to prodn	Jim Fehrle

2020-11-09	Add global version of OPTINREF	Jim Fehrle

2020-11-09	Merge PR #13329: [refman] Stop applying a special style to Coq, CoqIDE, ↵	coqbot-app[bot]
	OCaml and Gallina. Reviewed-by: jfehrle Reviewed-by: cpitclaudel
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-09	Fix #5226: Add index entry for ::=.	Théo Zimmermann

2020-11-09	Fix indentation of todo in Ltac chapter.	Théo Zimmermann
	Actual documentation was interpreted as a comment.
2020-11-06	Intro pattern extensions for dup, swap and apply	Cyril Cohen

2020-11-05	Add a redirection from previous location of the proof handling chapter.	Théo Zimmermann

2020-11-05	Various fixes.	Théo Zimmermann

2020-11-05	Merge content from two origins into the same file.	Théo Zimmermann

2020-11-05	Move proof handling chapter in new location.	Théo Zimmermann

2020-11-05	Remove parts of Tactics that were moved elsewhere.	Théo Zimmermann

2020-11-04	Regenerate the grammar description file.	Pierre-Marie Pédrot

2020-11-04	Document the syntax addition.	Pierre-Marie Pédrot

2020-11-02	[doc] attribute #[using]	Enrico Tassi

2020-10-27	Change a few nonterminal names in mlgs and update doc to match	Jim Fehrle

2020-10-27	Rename misc nonterminals	Jim Fehrle

2020-10-24	Convert misc chapters to prodn	Jim Fehrle

2020-10-20	Add some missing smallcaps.	Théo Zimmermann

2020-10-15	Merge PR #13140: Documenting Set Printing Goal Names + a small goal display fix	coqbot-app[bot]
	Reviewed-by: ejgallego Reviewed-by: Zimmi48
2020-10-12	Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocol	coqbot-app[bot]
	Reviewed-by: herbelin Ack-by: gares Ack-by: ejgallego
2020-10-09	Add an XML message for "Show Proof Diffs"	Jim Fehrle
	Add menu item that uses this
2020-10-06	Documenting option Set Printing Goal Name.	Hugo Herbelin

2020-10-02	{new,setoid_}ring -> ring	Maxime Dénès
	I believe this renaming makes it easier for new contributors to discover the code of `ring`.
2020-09-18	Make `simple apply in ...` point to `simple apply`	Maxime Dénès
	Instead, the example was duplicated.
2020-09-18	Improve `simple apply` example	Maxime Dénès
	The example showing the difference between `apply` and `simple apply` used to depend on the order and the heuristics used on unification problems. We make it independent for better clarity and stability. Fixes https://github.com/coq/coq/issues/13023
2020-09-11	Turn integer into natural in several mlgs	Pierre Roux
	Negative values had no meaning there. Those were spotted by Hugo Herbelin while reviewing #12979 .
2020-09-11	[refman] Rename int to integer	Pierre Roux

2020-09-11	[refman] Rename num to natural	Pierre Roux

2020-09-11	[refman] Replace num by int	Pierre Roux
	num stands for natural numbers whereas the text deals with negative values.
2020-09-11	Minimal changes to make the refman compatible with Sphinx 3.	Théo Zimmermann
	Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-09-08	Merge PR #12993: Remove deprecated tactic cutrewrite.	Clément Pit-Claudel
	Reviewed-by: cpitclaudel Reviewed-by: ppedrot
2020-09-08	Remove deprecated tactic cutrewrite.	Théo Zimmermann

2020-09-08	Merge PR #12931: Proof using cleanup, small doc addition and fix using Type ↵	coqbot-app[bot]
	in collections Reviewed-by: gares Ack-by: Zimmi48
2020-09-07	Explain how selectors change the order of goals	Jim Fehrle

2020-08-28	Proof using cleanup, small doc addition and fix using Type in collections	Gaëtan Gilbert
	Fix #12930
2020-08-26	Merge PR #12085: Convert ltac2 chapter to use prodn, update syntax	coqbot-app[bot]
	Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle Ack-by: ppedrot
2020-08-25	Convert ltac2 chapter to use prodn, update syntax	Jim Fehrle

2020-08-17	Recommend replace as a replacement to cutrewrite.	Théo Zimmermann
	As suggested by Laurent Thery to Chris Dams on Coq-Club. (And fix the documented syntax in the manual.)
2020-08-10	Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)	Cyril Cohen
	Reviewed-by: CohenCyril Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: maximedenes Ack-by: ppedrot
2020-08-10	[ssr] turn "nothing to inject" into a real warning (fix #12746)	Enrico Tassi

2020-08-07	Merge PR #12643: Document "Print Debug GC" command and OCAMLRUNPARAM ↵	coqbot
	environment variable Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-08-04	Document "Print Debug GC" command and OCAMLRUNPARAM env variable	Jim Fehrle

2020-07-29	Fix do in ssreflect-proof-language.rst	Yusuke Matsushita
	The tactics do in SSReflect uses `? @mult` rather than `? @num`.
2020-07-11	tactics.rst: `Require A` is enough for `A`'s hints	Paolo G. Giarrusso
	As the text says later: > Hints should only be made available when the module they are defined in is imported, not just required.
2020-06-17	tactics.rst: readd `cbv`	Paolo G. Giarrusso
	Hope this is enough, also looking at https://github.com/coq/coq/commit/4c9ba141f8f7e067f274cb5a02293e8e52f89487#diff-a907eea979c6d310cb6208180b556d6d.