]> matita.cs.unibo.it Git - helm.git/tree - helm/software/components/tactics/
The signature in "retrieve equations" must be extended with the equality if
[helm.git] / helm / software / components / tactics /
drwxr-xr-x   ..
-rw-r--r-- 11708 .depend
-rw-r--r-- 11708 .depend.opt
-rw-r--r-- 2023 Makefile
-rw-r--r-- 68351 auto.ml
-rw-r--r-- 2329 auto.mli
-rw-r--r-- 5376 autoCache.ml
-rw-r--r-- 1697 autoCache.mli
-rw-r--r-- 1931 autoTypes.ml
-rw-r--r-- 1648 autoTypes.mli
-rw-r--r-- 18033 closeCoercionGraph.ml
-rw-r--r-- 1561 closeCoercionGraph.mli
-rw-r--r-- 6787 compose.ml
-rw-r--r-- 1168 compose.mli
-rw-r--r-- 11797 continuationals.ml
-rw-r--r-- 3551 continuationals.mli
-rw-r--r-- 10458 declarative.ml
-rw-r--r-- 2452 declarative.mli
-rw-r--r-- 24390 destructTactic.ml
-rw-r--r-- 1295 destructTactic.mli
drwxr-xr-x - doc
-rw-r--r-- 6612 eliminationTactics.ml
-rw-r--r-- 1285 eliminationTactics.mli
-rw-r--r-- 14542 equalityTactics.ml
-rw-r--r-- 1582 equalityTactics.mli
-rw-r--r-- 7658 fourier.ml
-rw-r--r-- 1088 fourier.mli
-rw-r--r-- 43416 fourierR.ml
-rw-r--r-- 170 fourierR.mli
-rw-r--r-- 6918 fwdSimplTactic.ml
-rw-r--r-- 1312 fwdSimplTactic.mli
-rw-r--r-- 20075 hashtbl_equiv.ml
-rw-r--r-- 1690 hashtbl_equiv.mli
-rw-r--r-- 2997 history.ml
-rw-r--r-- 1147 history.mli
-rw-r--r-- 1987 introductionTactics.ml
-rw-r--r-- 1200 introductionTactics.mli
-rw-r--r-- 12787 inversion.ml
-rw-r--r-- 1226 inversion.mli
-rw-r--r-- 7796 inversion_principle.ml
-rw-r--r-- 23 inversion_principle.mli
-rw-r--r-- 18356 metadataQuery.ml
-rw-r--r-- 2569 metadataQuery.mli
-rw-r--r-- 3556 negationTactics.ml
-rw-r--r-- 1094 negationTactics.mli
drwxr-xr-x - paramodulation
-rw-r--r-- 42117 primitiveTactics.ml
-rw-r--r-- 3629 primitiveTactics.mli
-rw-r--r-- 27344 proofEngineHelpers.ml
-rw-r--r-- 5484 proofEngineHelpers.mli
-rw-r--r-- 36068 proofEngineReduction.ml
-rw-r--r-- 3306 proofEngineReduction.mli
-rw-r--r-- 7283 proofEngineStructuralRules.ml
-rw-r--r-- 1302 proofEngineStructuralRules.mli
-rw-r--r-- 3415 proofEngineTypes.ml
-rw-r--r-- 2702 proofEngineTypes.mli
-rw-r--r-- 8894 reductionTactics.ml
-rw-r--r-- 1814 reductionTactics.mli
-rw-r--r-- 22498 ring.ml
-rw-r--r-- 272 ring.mli
-rw-r--r-- 71699 setoids.ml
-rw-r--r-- 2770 setoids.mli
-rw-r--r-- 7214 statefulProofEngine.ml
-rw-r--r-- 4292 statefulProofEngine.mli
-rw-r--r-- 9338 tacticChaser.ml
-rw-r--r-- 9695 tacticals.ml
-rw-r--r-- 1902 tacticals.mli
-rw-r--r-- 3053 tactics.ml
-rw-r--r-- 4442 tactics.mli
-rw-r--r-- 5112 universe.ml
-rw-r--r-- 2105 universe.mli
-rw-r--r-- 2184 variousTactics.ml
-rw-r--r-- 1034 variousTactics.mli