]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 511421f) | patch
Constants are indexed using the Reference, not the Uri, so that constructors
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 2 Mar 2010 11:53:57 +0000 (11:53 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 2 Mar 2010 11:53:57 +0000 (11:53 +0000)
commit2b52dcc1742d2ee0616b6526e3ade1dd21ec10f3
tree60140e0f0722e0085e8b70c782c04d60ba54d6datree | snapshot
parent511421f12dd04547bbf1206470e5d39237673429commit | diff
Constants are indexed using the Reference, not the Uri, so that constructors
are different!
helm/software/components/ng_refiner/nDiscriminationTree.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.