coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-06-30	[states] Move States to vernac	Emilio Jesus Gallego Arias
	We continue to push state layers upwards, in preparation of a functional vernacular interpretation. Now we move `States` and `Printmod` which messes with the global state as to temporarily create envs with modules.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-09-18	[library] Move `Declaremods` to `vernac/`	Emilio Jesus Gallego Arias
	We move `Declaremods` to the vernac layer as it implement vernac-specific logic to manipulate modules which moreover is highly imperative. This forces code [such as printing] to manipulate the _global imperative_ state which is a bit fishy. The key improvement in this PR is that now `Global` is not used anymore in `library`, so we can proceed to move it upwards. This move is a follow-up of #10562 and a step towards moving `Global` upper, likely to `interp` in the short term.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2018-05-17	Split off Universes functions dealing with names.	Gaëtan Gilbert
	This API is a bit strange, I expect it will change at some point.
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-11-25	Allow local universe renaming in Print.	Gaëtan Gilbert

2017-11-06	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias
	This will allow to merge back `Names` with `API.Names`
2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2017-03-21	[pp] Remove unused printing tagging infrastructure.	Emilio Jesus Gallego Arias
	Applications of it were not clear/unproven, it made printers more complex (as they needed to be functors) and as it lacked examples it confused some people. The printers now tag unconditionally, it is up to the backends to interpreted the tags. Tagging (and indeed the notion of rich document) should be reworked in a follow-up patch, so they are in sync, but this is a first step. Tested, test-suite passes. Notes: - We remove the `Richprinter` module. It was only used in the `annotate` IDE protocol call, its output was identical to the normal printer (or even inconsistent if taggers were not kept manually in sync). - Note that Richpp didn't need a single change. In particular, its main API entry point `Richpp.rich_pp` is not used by anyone.
2016-01-20	Update copyright headers.	Maxime Dénès

2015-01-12	Update headers.	Maxime Dénès

2014-11-19	Adding rich-printing facilities to Printmod.	Pierre-Marie Pédrot

2013-02-19	Dir_path --> DirPath	letouzey
	Ok, this is merely a matter of taste, but up to now the usage in Coq is rather to use capital letters instead of _ in the names of inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-12-14	Modulification of dir_path	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08	Updating headers.	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29	place all pretty-printing files in new dir printing/	letouzey
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15391 85f007b7-540e-0410-9357-904b9bb8a0f7