aboutsummaryrefslogtreecommitdiff
path: root/lib/hashcons.mli
AgeCommit 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-04Bump year in headers.Pierre-Marie Pédrot
2016-03-22A patch renaming equal into eq in the module dealing withHugo Herbelin
hash-consing, so as to avoid having too many kinds of equalities with same name.
2016-01-20Update copyright headers.Maxime Dénès
2015-08-02Reverting 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-02A patch renaming equal into eq in the module dealing withHugo Herbelin
hash-consing, so as to avoid having too many kinds of equalities with same name.
2015-02-11Adding a statistic function on hashconsing tables.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-17Ensuring the good invariants of hashcons table generation in the API.Pierre-Marie Pédrot
2013-10-24Specializing hash functions for widely used types.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16933 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-28Removing some lone List.assoc & List.mem in lib.ppedrot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16738 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22More complete hashcons : lists (dirpath), arrays (constr)letouzey
Earlier, the elements of constr arrays were hash-consed, but not the array itself. This helps a bit when the same (f a1 ... an) is manipulated a lot : -20% in the size of opaque terms in Integral_domain.vo and Nsatz.vo Similarly it's interesting to hash-cons sub-lists for dirpaths, since in Coq.A.B and Coq.A.C we could share Coq.A. With this patch, the hash-consing of constr seems quasi-optimal: Pierre-Marie's marshal compactor is unable to shrink opaque tables by more than 2%, and this difference seems to be due to untyped compaction (for the compactor Rel 1 = Prop Pos). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16723 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-17Using 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-26Reusing the Hashset data structure in Hashcons. Hopefully, this shouldppedrot
not disrupt anything... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15836 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-26Cleaning, 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
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
dev/ocamlweb-doc has been erased. I hope no one still use the "new-parse" it generate. In dev/, make html will generate in dev/html/ "clickable version of mlis". (as the caml standard library) make coq.pdf will generate nearly the same awfull stuff that coq.ps was. make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of the given directory. ocamldoc comment syntax is here : http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html The possibility to put graphs in pdf/html seems to be lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-09-19 - un effort sur la doc (ocamlweb)filliatr
- module Nametab - module Impargs - correction bug : Parameter id : t => vérification que t est bien un type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@76 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-08-30un petit effort de presentation dans les interfacesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@31 85f007b7-540e-0410-9357-904b9bb8a0f7
1999-08-16Initial revisionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:02:08 +0000