]> matita.cs.unibo.it Git - helm.git/tree - helm/software/components/tactics/paramodulation/
occur_check and unification fixed. now Meta(i,[]) and Meta(i,[...]) are
[helm.git] / helm / software / components / tactics / paramodulation /
drwxr-xr-x   ..
-rw-r--r-- 0 .depend
-rw-r--r-- 42 Makefile
-rw-r--r-- 1493 README
-rw-r--r-- 33140 equality.ml
-rw-r--r-- 3687 equality.mli
-rw-r--r-- 4551 equality_indexing.ml
-rw-r--r-- 1604 equality_indexing.mli
-rw-r--r-- 40171 indexing.ml
-rw-r--r-- 2840 indexing.mli
-rw-r--r-- 17098 inference.ml
-rw-r--r-- 2676 inference.mli
-rw-r--r-- 62948 saturation.ml
-rw-r--r-- 1887 saturation.mli
-rw-r--r-- 6921 subst.ml
-rw-r--r-- 1759 subst.mli
-rw-r--r-- 8703 test_indexing.ml
-rw-r--r-- 20719 utils.ml
-rw-r--r-- 2662 utils.mli