]> matita.cs.unibo.it Git - helm.git/tree - helm/software/components/ng_tactics/
Equality has one right parameter and thus it's elimination principle has two
[helm.git] / helm / software / components / ng_tactics /
drwxr-xr-x   ..
-rw-r--r-- 1322 .depend
-rw-r--r-- 1322 .depend.opt
-rw-r--r-- 336 Makefile
-rw-r--r-- 825 README
-rw-r--r-- 2483 andOrTree.ml
-rw-r--r-- 2155 andOrTree.mli
-rw-r--r-- 56657 nAuto.ml
-rw-r--r-- 1036 nAuto.mli
-rw-r--r-- 10723 nCicElim.ml
-rw-r--r-- 943 nCicElim.mli
-rw-r--r-- 1092 nCicTacReduction.ml
-rw-r--r-- 803 nCicTacReduction.mli
-rw-r--r-- 21385 nDestructTac.ml
-rw-r--r-- 747 nDestructTac.mli
-rw-r--r-- 7298 nInversion.ml
-rw-r--r-- 863 nInversion.mli
-rw-r--r-- 17884 nTacStatus.ml
-rw-r--r-- 4505 nTacStatus.mli
-rw-r--r-- 21784 nTactics.ml
-rw-r--r-- 4201 nTactics.mli
-rw-r--r-- 48560 nnAuto.ml
-rw-r--r-- 1229 nnAuto.mli
-rw-r--r-- 4014 zipTree.ml
-rw-r--r-- 1609 zipTree.mli