]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4fcebf3) | patch
The hash-table used in the implementation was of "type"
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 13 Dec 2001 12:09:17 +0000 (12:09 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 13 Dec 2001 12:09:17 +0000 (12:09 +0000)
commit20dacdd66818f115aab029824b7408c0d4f804c4
tree641a5c2f851d6fcda641f10a63d83472257e7a6ftree | snapshot
parent4fcebf318b866ce041b31d7ac4ddb0fdb29d098dcommit | diff
The hash-table used in the implementation was of "type"
(UriManager.uri * int) -> Cic.obj

Is is now of type
UriManager.uri -> (int * Cic.obj) list

where the list is ordered from the most cooked to the less cooked.

There is almost no difference at all in the performance of big files
(limit_plus). The new design is easier to extend to a real cache with
rollback.
helm/ocaml/cic_proof_checking/cicEnvironment.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.