]> matita.cs.unibo.it Git - helm.git/tree - helm/ocaml/tactics/
1. ProofEngineHelpers.locate_in_term, ProofEngineHelpers.locate_in_conjecture
[helm.git] / helm / ocaml / tactics /
drwxr-xr-x   ..
-rw-r--r-- 59 .cvsignore
-rw-r--r-- 6490 .depend
-rw-r--r-- 827 Makefile
-rw-r--r-- 11609 autoTactic.ml
-rw-r--r-- 1294 autoTactic.mli
-rw-r--r-- 30317 discriminationTactics.ml
-rw-r--r-- 1220 discriminationTactics.mli
-rw-r--r-- 9415 eliminationTactics.ml
-rw-r--r-- 1327 eliminationTactics.mli
-rw-r--r-- 11123 equalityTactics.ml
-rw-r--r-- 1528 equalityTactics.mli
-rw-r--r-- 7658 fourier.ml
-rw-r--r-- 1088 fourier.mli
-rw-r--r-- 43479 fourierR.ml
-rw-r--r-- 170 fourierR.mli
-rw-r--r-- 5850 fwdSimplTactic.ml
-rw-r--r-- 1293 fwdSimplTactic.mli
-rw-r--r-- 20064 hashtbl_equiv.ml
-rw-r--r-- 1690 hashtbl_equiv.mli
-rw-r--r-- 2985 history.ml
-rw-r--r-- 1147 history.mli
-rw-r--r-- 1958 introductionTactics.ml
-rw-r--r-- 1200 introductionTactics.mli
-rw-r--r-- 22626 metadataQuery.ml
-rw-r--r-- 2414 metadataQuery.mli
-rw-r--r-- 3074 negationTactics.ml
-rw-r--r-- 1094 negationTactics.mli
-rw-r--r-- 21545 primitiveTactics.ml
-rw-r--r-- 1971 primitiveTactics.mli
-rw-r--r-- 27611 proofEngineHelpers.ml
-rw-r--r-- 4731 proofEngineHelpers.mli
-rw-r--r-- 35575 proofEngineReduction.ml
-rw-r--r-- 1966 proofEngineReduction.mli
-rw-r--r-- 5802 proofEngineStructuralRules.ml
-rw-r--r-- 1212 proofEngineStructuralRules.mli
-rw-r--r-- 2496 proofEngineTypes.ml
-rw-r--r-- 2187 proofEngineTypes.mli
-rw-r--r-- 7471 reductionTactics.ml
-rw-r--r-- 1691 reductionTactics.mli
-rw-r--r-- 22502 ring.ml
-rw-r--r-- 272 ring.mli
-rw-r--r-- 6953 statefulProofEngine.ml
-rw-r--r-- 4174 statefulProofEngine.mli
-rw-r--r-- 9323 tacticChaser.ml
-rw-r--r-- 9654 tacticals.ml
-rw-r--r-- 2127 tacticals.mli
-rw-r--r-- 2971 tactics.ml
-rw-r--r-- 3673 tactics.mli
-rw-r--r-- 6460 variousTactics.ml
-rw-r--r-- 1221 variousTactics.mli