]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6f6ce52) | patch
1. profiling code added
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 21 Sep 2005 08:35:56 +0000 (08:35 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 21 Sep 2005 08:35:56 +0000 (08:35 +0000)
commit6849a0b7b65075049427c27f60d19210ddb52cf5
tree69ac7e6e658e87dab0236e6a3ed26844e4e677a5tree | snapshot
parent6f6ce528977597b1745e97a1cb3778d3335b8133commit | diff
1. profiling code added
2. debug_print made lazy to avoid computation of the argument when profiling
   is disabled. This really speeds up disambiguation!
helm/ocaml/cic_disambiguation/disambiguate.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.