coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-04-22	Add changelog	Pierre Roux

2021-03-04	Properly support nested timeouts	Lasse Blaauwbroek

2020-12-03	[changelog] update markup	Enrico Tassi

2020-12-03	Changes for Coq 8.13	Matthieu Sozeau

2020-11-26	[attributes] [doc] Documentation review by Théo.	Emilio Jesus Gallego Arias
	Co-authored-by: <Théo Zimmermann <theo.zimmermann@inria.fr>
2020-11-26	[vernac] Allow to control typing flags with attributes.	Emilio Jesus Gallego Arias
	The syntax is the one of boolean attributes, that is to say `#[typing($flag={yes,no}]` where `$flag` is one of `guarded`, `universes`, `positive`. We had to instrument the pretyper in a few places, it is interesting that it is doing so many checks.
2020-11-26	[declare] Allow custom typing flags when declaring constants.	Emilio Jesus Gallego Arias
	We use the new `Declare.Info` structure to uniformly add properties to the handling of constants. In this case, per-constant typing flags. The internal code may want to see some further refactoring, including pushing the flags down to `Safe_typing.add_constant` , but the changes in the interface should be definitive. This will allow #12539 and #9004 using attributes.
2020-11-24	Add a changelog.	Pierre-Marie Pédrot

2020-05-27	Release notes for 8.12.	Théo Zimmermann

2020-05-14	[exn] [tactics] improve backtraces on monadic errors	Emilio Jesus Gallego Arias
	Current backtraces for tactics leave a bit to desire, for example given the program: ```coq Lemma u n : n + 0 = n. rewrite plus_O_n. ``` the backtrace stops at: ``` Found no subterm matching "0 + ?M160" in the current goal. Called from file "proofs/proof.ml", line 381, characters 4-42 Called from file "tactics/pfedit.ml", line 102, characters 31-58 Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84 ``` Backtrace information `?info` is as of today optional in some tactics, such as `tclZERO`, it doesn't cost a lot however to reify backtrace information indeed in `tclZERO` and provide backtraces for all tactic errors. The cost should be small if we are not in debug mode. The backtrace for the failed rewrite is now: ``` Found no subterm matching "0 + ?M160" in the current goal. Raised at file "pretyping/unification.ml", line 1827, characters 14-73 Called from file "pretyping/unification.ml", line 1929, characters 17-53 Called from file "pretyping/unification.ml", line 1948, characters 22-72 Called from file "pretyping/unification.ml", line 2020, characters 14-56 Re-raised at file "pretyping/unification.ml", line 2021, characters 66-73 Called from file "proofs/clenv.ml", line 254, characters 12-58 Called from file "proofs/clenvtac.ml", line 95, characters 16-53 Called from file "engine/proofview.ml", line 1110, characters 40-46 Called from file "engine/proofview.ml", line 1115, characters 10-34 Re-raised at file "clib/exninfo.ml", line 82, characters 4-38 Called from file "proofs/proof.ml", line 381, characters 4-42 Called from file "tactics/pfedit.ml", line 102, characters 31-58 Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84 ``` which IMO is much better.
2020-04-03	Adding changelog for 8.11.1.	Pierre-Marie Pédrot

2020-03-08	Minor improvements to the unreleased changelog.	Théo Zimmermann

2020-02-20	Adding changelog.	Hugo Herbelin

2020-01-08	Add changelog entry for native string extraction	Maxime Dénès

2019-06-16	Changelog for 8.10+beta2.	Théo Zimmermann

2019-06-03	Update doc to reflect that PG now supports Coq-generated proof diffs	Jim Fehrle

2019-05-13	Move last changelog entries for 8.10+beta1.	Théo Zimmermann

2019-05-08	Update release process documentation and changelog entry.	Théo Zimmermann

2019-05-05	Add changelog entry about moving changelog to refman.	Théo Zimmermann

2019-05-05	Create categories in changelog.	Théo Zimmermann