]> matita.cs.unibo.it Git - helm.git/tree - helm/ocaml/tactics/paramodulation/
Added recursive path ordering and demodulation tactic.
[helm.git] / helm / ocaml / tactics / paramodulation /
drwxr-xr-x   ..
-rw-r--r-- 594 .depend
-rw-r--r-- 459 Makefile
-rw-r--r-- 1493 README
-rw-r--r-- 4249 equality_indexing.ml
-rw-r--r-- 1608 equality_indexing.mli
-rw-r--r-- 37546 indexing.ml
-rw-r--r-- 3064 indexing.mli
-rw-r--r-- 31176 inference.ml
-rw-r--r-- 4557 inference.mli
-rw-r--r-- 5891 saturate_main.ml
-rw-r--r-- 81040 saturation.ml
-rw-r--r-- 1726 saturation.mli
-rw-r--r-- 8703 test_indexing.ml
-rw-r--r-- 18800 utils.ml
-rw-r--r-- 2606 utils.mli