]> matita.cs.unibo.it Git - helm.git/tree - helm/ocaml/tactics/
Generalize now works on a list of convertible terms, generalizing all of
[helm.git] / helm / ocaml / tactics /
drwxr-xr-x   ..
-rw-r--r-- 39 .cvsignore
-rw-r--r-- 3656 .depend
-rw-r--r-- 744 Makefile
-rw-r--r-- 8405 eliminationTactics.ml
-rw-r--r-- 1345 eliminationTactics.mli
-rw-r--r-- 8793 equalityTactics.ml
-rw-r--r-- 1475 equalityTactics.mli
-rw-r--r-- 7658 fourier.ml
-rw-r--r-- 1088 fourier.mli
-rw-r--r-- 42080 fourierR.ml
-rw-r--r-- 170 fourierR.mli
-rw-r--r-- 1791 introductionTactics.ml
-rw-r--r-- 1200 introductionTactics.mli
-rw-r--r-- 2800 negationTactics.ml
-rw-r--r-- 1094 negationTactics.mli
-rw-r--r-- 22838 primitiveTactics.ml
-rw-r--r-- 1619 primitiveTactics.mli
-rw-r--r-- 5418 proofEngineHelpers.ml
-rw-r--r-- 2052 proofEngineHelpers.mli
-rw-r--r-- 31816 proofEngineReduction.ml
-rw-r--r-- 1889 proofEngineReduction.mli
-rw-r--r-- 5440 proofEngineStructuralRules.ml
-rw-r--r-- 1109 proofEngineStructuralRules.mli
-rw-r--r-- 1672 proofEngineTypes.ml
-rw-r--r-- 4570 reductionTactics.ml
-rw-r--r-- 1493 reductionTactics.mli
-rw-r--r-- 22450 ring.ml
-rw-r--r-- 272 ring.mli
-rw-r--r-- 7411 tacticals.ml
-rw-r--r-- 1776 tacticals.mli
-rw-r--r-- 6024 variousTactics.ml
-rw-r--r-- 1281 variousTactics.mli