coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-04-29	Merge the call to tclEFFECTS into find_scheme.	Pierre-Marie Pédrot
	This encapsulates better the invariants of this function.
2020-04-28	Return an option in lookup_scheme.	Pierre-Marie Pédrot

2020-04-28	Stop relying on side-effects for recursive scheme declaration.	Pierre-Marie Pédrot
	Instead, we register functions dynamically declaring the dependencies of the scheme to be generated. We had to fix the test-suite because an internal scheme name changed. We could also tweak the internal flag of scheme dependencies, but in this particular case it looks more like a bug from the previous implementation.
2020-04-21	[declare] [tactics] Move declare to `vernac`	Emilio Jesus Gallego Arias
	This PR moves `Declare` to `vernac` which will hopefully allow to unify it with `DeclareDef` and avoid exposing entry internals. There are many tradeoffs to be made as interface and placement of tactics is far from clear; I've tried to reach a minimally invasive compromise: - moved leminv to `ltac_plugin`; this is unused in the core codebase and IMO for now it is the best place - hook added for abstract; this should be cleaned up later - hook added for scheme declaration; this should be cleaned up later - separation of hints vernacular and "tactic" part should be also done later, for now I've introduced a `declareUctx` module to avoid being invasive there. In particular this last point strongly suggest that for now, the best place for `Class_tactics` would be also in `ltac`, but I've avoided that for now too. This partially supersedes #10951 for now and helps with #11492 .
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-12-10	Side-effect free wrapper around already declared schemes.	Pierre-Marie Pédrot
	Some calls are actually guarded by a check that the scheme is already in the cache. There is no reason to generate dummy side-effects in that case.
2019-12-10	Make explicit that users should not observe return values of scheme functions.	Pierre-Marie Pédrot

2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
	We also remove trailing whitespace. Script used: ```bash for i in `find . -name '.ml' -or -name '.mli' -or -name '.mlg'`; do expand -i "$i" \| sponge "$i"; sed -e's/[[:space:]]$//' -i.bak "$i"; done ```
2019-10-30	[declare] Remove declare_scheme hook in Declare	Emilio Jesus Gallego Arias
	We introduce a new module that registers the scheme information that side-effects need, thus removing the hook from `Declare`. As we may want to deprecate scheme side effects, there is no need to design a general mechanism for this kind of registration for now. Would we remove the scheme side-effects the scheme code could become self-contained again.
2019-06-25	Move the internal_flag type from Declare to Ind_tables.	Pierre-Marie Pédrot
	It is completely local to that file, there was no point to put it into the unrelated Declare file.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-06-11	Remove the side-effect role from the kernel.	Pierre-Marie Pédrot
	We move the role data into the evarmap instead.
2018-02-27	Update headers following #6543.	Théo Zimmermann

2017-11-06	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias
	We do up to `Term` which is the main bulk of the changes.
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-19	[general] Move files to directories matching linking order.	Emilio Jesus Gallego Arias
	We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`, `Miscprint`) to their proper place as they were declared in different `mllib` files than the one in their directory. In some cases this could be refined but we don't do anything fancy, we just reflect the status quo.