]> matita.cs.unibo.it Git - helm.git/commit
more abstract discrimination tree
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 19 Sep 2008 12:47:23 +0000 (12:47 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 19 Sep 2008 12:47:23 +0000 (12:47 +0000)
commiteaf5880ed69963b3ad37cb1f8a1fd48b2918e58b
tree91a3a8efe44cddfc0318b35c6267e012687ceb49
parentff5d621723a60609c67152c110b8386f7902c1ff
more abstract discrimination tree
helm/software/components/cic/discrimination_tree.ml
helm/software/components/cic/discrimination_tree.mli
helm/software/components/ng_refiner/nDiscriminationTree.ml
helm/software/components/ng_refiner/nDiscriminationTree.mli
helm/software/components/tactics/paramodulation/equality_indexing.ml
helm/software/components/tactics/paramodulation/equality_indexing.mli
helm/software/components/tactics/paramodulation/indexing.mli
helm/software/components/tactics/universe.ml