]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 65d6937) | patch
WARNING: major experimental change.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 11 Oct 2011 10:43:54 +0000 (10:43 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 11 Oct 2011 10:43:54 +0000 (10:43 +0000)
commitd72aaf7d3c12ecc70208a896e08b120b5031a7cb
tree1c2e6df6fd8cd26f5f4a0e026698eb81f0045293tree | snapshot
parent65d69375785f5e6ed48c944cdc3b4a526b5913e3commit | diff
WARNING: major experimental change.

"include" is no longer turned into an "include alias"
when the file to be included is already loaded. This
greatly speeds up inclusion, at the price of having
to manually add some "include alias" here and there.
matita/components/ng_library/nCicLibrary.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.