coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-05-31	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias
	Continuing the interface cleanup we place `Constrexpr` in the internalization module, which is the one that eliminates it. This slims down `pretyping` considerably, including removing the `Univdecls` module which existed only due to bad dependency ordering in the first place. Thanks to @ Skyskimmer we also remove a duplicate `univ_decl` definition among `Misctypes` and `UState`. This is mostly a proof of concept yet as it depends on quite a few patches of the tree. For sure some tweaks will be necessary, but it should be good for review now. IMO the tree is now in a state where we can could easy eliminate more than 10 modules without any impact, IMHO this is a net saving API-wise and would help people to understand the structure of the code better.
2018-02-27	Update headers following #6543.	Théo Zimmermann

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

2017-05-27	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias
	This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey
	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
2016-07-01	Add and document match, fix and cofix reduction flags.	Maxime Dénès

2016-01-20	Update copyright headers.	Maxime Dénès

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

2013-10-23	cList: set-as-list functions are now with an explicit comparison	letouzey
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ↵	xclerc
	with OCaml 3.12.1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16787 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot
	List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 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	Glob_term now mli-only, operations now in Glob_ops	letouzey
	Stuff about reductions now in genredexpr.mli, operations in redops.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 85f007b7-540e-0410-9357-904b9bb8a0f7