coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2019-01-25	[Numeral notations] Use Coqlib registered constants	Vincent Laporte

2018-10-10	[coqlib] Rebindable Coqlib namespace.	Emilio Jesus Gallego Arias
	We refactor the `Coqlib` API to locate objects over a namespace `module.object.property`. This introduces the vernacular command `Register g as n` to expose the Coq constant `g` under the name `n` (through the `register_ref` function). The constant can then be dynamically located using the `lib_ref` function. Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org> Co-authored-by: Maxime Dénès <mail@maximedenes.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2018-09-10	Adapting standard library to the introduction of "Declare Scope".	Hugo Herbelin
	Removing in passing two Local which are no-ops in practice.
2018-08-31	Numeral Notation for nat	Pierre Letouzey
	This parsing/printing method for nat should be just as fast as the previous dedicated code. Moreover, we could now parse large literals as nat numbers, by leaving them in a half-abstract form such as (Nat.of_uint 123456). This form is convertible to the closed (S (S (S ...))) form, so it shouldn't be a big deal for compatibility, except for if some Ltac stuff relies on (S ...) to be present after parsing. Of course, forcing the computation of a (Nat.of_uint ....) may take a while or raise a Stack Overflow.
2018-06-29	Splitting primitive numeral parser/printer for positive, N, Z into three files.	Hugo Herbelin

2018-02-27	Update headers following #6543.	Théo Zimmermann

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

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

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

2013-07-17	"Boolean Equality" and "Case Analysis" are already off by default...	letouzey
	... no need to Unset them manually git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16631 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
2011-11-21	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-05-05	Definitions of positive, N, Z moved in Numbers/BinNums.v	letouzey
	In the coming reorganisation, the name Z in BinInt will be a module containing all code and properties about binary integers. The inductive type Z hence cannot be at the same location. Same for N and positive. Apart for this naming constraint, it also have advantages : presenting the three types at once is clearer, and we will be able to refer to N in BinPos (for instance for output type of a predecessor function on positive). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14097 85f007b7-540e-0410-9357-904b9bb8a0f7