coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-11-09	Remove the native symbol registering from the safe environment.	Pierre-Marie Pédrot
	Instead we store that data in the native code that was generated in adapt the compilation scheme accordingly. Less indirections and less imperative tinkering makes the code safer. The global symbol table was originally introduced in #10359 as a way not to depend on the Global module in the generated code. By storing all the native-related information in the cmxs file itself, this PR also makes other changes easier, such as e.g. #13287.
2020-06-30	[declaremods] Remove abstraction of imperative module operations	Emilio Jesus Gallego Arias
	Now that `Printmods` is above `Declaremods`, we don't need to pass the extra `mod_ops` argument.
2020-04-13	pass filters around	Gaëtan Gilbert

2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-10-31	[prettyp] remove `mod_ops` and `indirect_accessor` parameters	Gaëtan Gilbert
	`Prettyp` is now late enough in linking to refer to them.
2019-09-18	[declaremods] Remove abstraction layer over module interpretation.	Emilio Jesus Gallego Arias
	Now that we place imperative module declaration on top of module interpretation we can remove the abstraction layer used in `Declaremods`, so the `interp_modast` parameter goes away. Improvement suggested by Gaëtan Gilbert.
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.