coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-02-25	[proof using] Remove duplicate code, refactor.	Emilio Jesus Gallego Arias
	PR #13183 introduced quite a bit of duplicate code, we refactor it and expose less internals on the way. That should make the API more robust.
2021-02-24	Infrastructure for fine-grained debug flags	Maxime Dénès

2020-11-02	attribute #[using] for Definition and Fixpoint	Enrico Tassi

2020-08-28	Proof using cleanup, small doc addition and fix using Type in collections	Gaëtan Gilbert
	Fix #12930
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-02-12	Remove Goptions.opt_name field	Gaëtan Gilbert
	The standard use is to repeat the option keywords in lowercase, which is basically useless. En passant add doc entry for Dump Arith.
2019-08-26	[glob/aux files] Remove undocumented Stdout dump, cleanup flags.	Emilio Jesus Gallego Arias
	Fixes #10640 We remove the `StdOut` dump target, so now dump will only happen if a file is specified. Indeed, we make the default no to dump, and enable dump only in coqc, moving the option to the `Coqcargs` module. No need for a changes entry as this feature was undocumented, and no use case was given when introduced. Output to feedback must be explicitly enabled by clients / coqidetop, and we have thus also removed the undocumented option `-feedback-glob`.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-04-12	Unify Set and Unset handling for options	Gaëtan Gilbert
	Not sure if the idetop.set_options was correctly changed, ocaml types pass at least.
2018-11-23	s/let _ =/let () =/ in some places (mostly goptions related)	Gaëtan Gilbert

2018-07-13	Remove useless libobject in proof_using	Maxime Dénès

2018-07-07	Introduce a Pcoq.Entry module for functions that ought to be exported.	Pierre-Marie Pédrot
	We deprecate the corresponding functions in Pcoq.Gram. The motivation is that the Gram module is used as an argument to Camlp5 functors, so that it is not stable by extension. Enforcing that its type is literally the one Camlp5 expects ensures robustness to extension statically. Some really internal functions have been bluntly removed. It is unlikely that they are used by external plugins.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2018-02-22	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias
	We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way.
2017-10-10	Parse [Proof using Type] without translating Type to an id.	Gaëtan Gilbert

2017-10-10	Use a nice printer for constant names in Suggest Proof Using.	Gaëtan Gilbert

2017-10-10	[vernac] Remove "Proof using" hacks from parser.	Emilio Jesus Gallego Arias
	We place `Proof_using` in the proper place [`vernac`] and we remove gross parsing hacks. The new placement should allow to use the printers and more convenient structure, and reduce strange coupling between parsing and internal representation.