coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-12-23	[lib] Split auxiliary libraries into Coq-specific and general.	Emilio Jesus Gallego Arias
	Up to this point the `lib` directory contained two different library archives, `clib.cma` and `lib.cma`, which a rough splitting between Coq-specific libraries and general-purpose ones. We know split the directory in two, as to make the distinction clear: - `clib`: contains libraries that are not Coq specific and implement common data structures and programming patterns. These libraries could be eventually replace with external dependencies and the rest of the code base wouldn't notice much. - `lib`: contains Coq-specific common libraries in widespread use along the codebase, but that are not considered part of other components. Examples are printing, error handling, or flags. In some cases we have coupling due to utility files depending on Coq specific flags, however this commit doesn't modify any files, but only moves them around, further cleanup is welcome, as indeed a few files in `lib` should likely be placed in `clib`. Also note that `Deque` is not used ATM.
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2016-03-22	A patch renaming equal into eq in the module dealing with	Hugo Herbelin
	hash-consing, so as to avoid having too many kinds of equalities with same name.
2016-01-20	Update copyright headers.	Maxime Dénès

2015-08-02	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin
	Sorry so much. Reverted: 707bfd5719b76d131152a258d49740165fbafe03. 164637cc3a4e8895ed4ec420e300bd692d3e7812. b9c96c601a8366b75ee8b76d3184ee57379e2620. 21e41af41b52914469885f40155702f325d5c786. 7532f3243ba585f21a8f594d3dc788e38dfa2cb8. 27fb880ab6924ec20ce44aeaeb8d89592c1b91cd. fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c. d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962. 6737055d165c91904fc04534bee6b9c05c0235b1. 342fed039e53f00ff8758513149f8d41fa3a2e99. 21525bae8801d98ff2f1b52217d7603505ada2d2. b78d86d50727af61e0c4417cf2ef12cbfc73239d. 979de570714d340aaab7a6e99e08d46aa616e7da. f556da10a117396c2c796f6915321b67849f65cd. d8226295e6237a43de33475f798c3c8ac6ac4866. fdab811e58094accc02875c1f83e6476f4598d26.
2015-08-02	A patch renaming equal into eq in the module dealing with	Hugo Herbelin
	hash-consing, so as to avoid having too many kinds of equalities with same name.
2015-02-11	Adding a statistic function on hashconsing tables.	Pierre-Marie Pédrot

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

2014-04-28	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin
	one_inductive_body so that when eta-expanding at "match" printing time we know if a let is part of the expected signature or part of the body. This is an easy fix for bugs like #3293. Another fix could be to enforce, as an invariant, or better syntactically, that "match"/"Case"'s have the body of their branches expanded.
2012-10-17	Using weak tables instead of plain hash tables while hashconsing.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15899 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-26	Reusing the Hashset data structure in Hashcons. Hopefully, this should	ppedrot
	not disrupt anything... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15836 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-26	Cleaning, renaming obscure functions and documenting in Hashcons.	ppedrot
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15834 85f007b7-540e-0410-9357-904b9bb8a0f7