]> matita.cs.unibo.it Git - helm.git/tree - helm/ocaml/tactics/
Merge of the V7_3_new_exportation branch.
[helm.git] / helm / ocaml / tactics /
drwxr-xr-x   ..
-rw-r--r-- 59 .cvsignore
-rw-r--r-- 4337 .depend
-rw-r--r-- 880 Makefile
-rw-r--r-- 33516 discriminationTactics.ml
-rw-r--r-- 1220 discriminationTactics.mli
-rw-r--r-- 9183 eliminationTactics.ml
-rw-r--r-- 1345 eliminationTactics.mli
-rw-r--r-- 8570 equalityTactics.ml
-rw-r--r-- 1475 equalityTactics.mli
-rw-r--r-- 7658 fourier.ml
-rw-r--r-- 1088 fourier.mli
-rw-r--r-- 39867 fourierR.ml
-rw-r--r-- 170 fourierR.mli
-rw-r--r-- 1802 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-- 5443 proofEngineHelpers.ml
-rw-r--r-- 2052 proofEngineHelpers.mli
-rw-r--r-- 32246 proofEngineReduction.ml
-rw-r--r-- 1899 proofEngineReduction.mli
-rw-r--r-- 5440 proofEngineStructuralRules.ml
-rw-r--r-- 1109 proofEngineStructuralRules.mli
-rw-r--r-- 1691 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-- 3773 tacticChaser.ml
-rw-r--r-- 1336 tacticChaser.mli
-rw-r--r-- 7447 tacticals.ml
-rw-r--r-- 1776 tacticals.mli
-rw-r--r-- 3469 variousTactics.ml
-rw-r--r-- 1207 variousTactics.mli