]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1e7b084) | patch
new discrimination tree instantiation with
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 8 Oct 2009 09:59:20 +0000 (09:59 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 8 Oct 2009 09:59:20 +0000 (09:59 +0000)
commitcf4b0ccb2b5d494f9c7856c7a849ca60ebf857cd
treeea28ab9ccf7cd3d830da7b88814971e197cc69f3tree | snapshot
parent1e7b084682623531f0a4b23618c6614c3a0c0436commit | diff
new discrimination tree instantiation with
inverse De Brujin indexes.
helm/software/components/ng_tactics/nTacStatus.ml diff | blob | history
helm/software/components/ng_tactics/nTacStatus.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.