coq - The formal proof system

Age	Commit message (Collapse)	Author
2021-04-06	Uniformizing the "already exists" messages	Hugo Herbelin

2021-01-28	vernac/declaremods: make object collection tail-recursive	Gabriel Scherer
	This patch is trying to upstream a jsCoq patch that was written to solve Stack Overflow issues: https://github.com/jscoq/jscoq/blob/v8.12/etc/patches/cps.patch It turns List.fold_right in vernac/declaremods into List.fold_left on a reversed lit.
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-20	Remove mod_constraints field of module body	Gaëtan Gilbert

2020-04-13	correctly open objects for Names filters	Gaëtan Gilbert

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.
2020-03-03	[exninfo] Deprecate aliases for exception re-raising.	Emilio Jesus Gallego Arias
	We make the primitives for backtrace-enriched exceptions canonical in the `Exninfo` module, deprecating all other aliases. At some point dependencies between `CErrors` and `Exninfo` were a bit complex, after recent clean-ups the roles seem much clearer so we can have a single place for `iraise` and `capture`.
2019-12-13	Use ~strict argument consistently in push_context/push_context_set intfs	Matthieu Sozeau
	One should generally push contexts with ~strict:true when the context is a monomorphic one (all univs > Set) except for template polymorphic inductives (>= Prop) and ~strict:false for universe polymorphic ones (>= Set). Includes fixes from Gaëtan's and Emilio's reviews
2019-11-05	Forbid Include inside sections	Gaëtan Gilbert
	This probably does not work well in general, and specifically avoids an anomaly fixing https://github.com/coq/coq/issues/10060
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-10-14	Remove obj_sec field of Nametab.obj_prefix record.	Gaëtan Gilbert
	There are no more users.
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.