]> matita.cs.unibo.it Git - helm.git/tree - components/tactics/paramodulation/
Naif substitution. Removed local context in metas during relocation.
[helm.git] / components / tactics / paramodulation /
drwxr-xr-x   ..
-rw-r--r-- 0 .depend
-rw-r--r-- 42 Makefile
-rw-r--r-- 1493 README
-rw-r--r-- 4231 equality_indexing.ml
-rw-r--r-- 1608 equality_indexing.mli
-rw-r--r-- 44506 indexing.ml
-rw-r--r-- 2841 indexing.mli
-rw-r--r-- 37936 inference.ml
-rw-r--r-- 4917 inference.mli
-rw-r--r-- 93890 saturation.ml
-rw-r--r-- 1837 saturation.mli
-rw-r--r-- 8703 test_indexing.ml
-rw-r--r-- 21031 utils.ml
-rw-r--r-- 2746 utils.mli