]> matita.cs.unibo.it Git - helm.git/tree - helm/ocaml/cic/
moved term indexing (in both discrimination and path tree forms) from paramodulation...
[helm.git] / helm / ocaml / cic /
drwxr-xr-x   ..
-rw-r--r-- 32 .cvsignore
-rw-r--r-- 1100 .depend
-rw-r--r-- 397 Makefile
-rw-r--r-- 11216 cic.ml
-rw-r--r-- 27829 cicParser.ml
-rw-r--r-- 1997 cicParser.mli
-rw-r--r-- 29177 cicUniv.ml
-rw-r--r-- 4084 cicUniv.mli
-rw-r--r-- 11806 cicUtil.ml
-rw-r--r-- 2272 cicUtil.mli
-rw-r--r-- 4617 deannotate.ml
-rw-r--r-- 1727 deannotate.mli
-rw-r--r-- 9063 discrimination_tree.ml
-rw-r--r-- 1425 discrimination_tree.mli
-rw-r--r-- 7075 helmLibraryObjects.ml
-rw-r--r-- 5380 helmLibraryObjects.mli
-rw-r--r-- 3965 libraryObjects.ml
-rw-r--r-- 1520 libraryObjects.mli
-rw-r--r-- 6258 path_indexing.ml
-rw-r--r-- 1410 path_indexing.mli
-rw-r--r-- 2985 test.ml
-rw-r--r-- 2830 unshare.ml
-rw-r--r-- 1024 unshare.mli