]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2e2648a) | patch
Do NOT dare using Pervasives.compare on data structures containing URIs!
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 23 Apr 2008 08:04:53 +0000 (08:04 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 23 Apr 2008 08:04:53 +0000 (08:04 +0000)
commit0805c61933df87f5cfae63b94456a1f0518b06d0
treec4659757a0e7a43b1722ba38d6fb1bd8f8881bb6tree | snapshot
parent2e2648a9ed26d9b813de8e6a10e2776162565f09commit | diff
Do NOT dare using Pervasives.compare on data structures containing URIs!
Use UriManager.compare to get a 2x speed-up in type-checking setoids.
helm/software/components/cic/cicUniv.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.