]> matita.cs.unibo.it Git - helm.git/tree - components/tactics/
decompose: delta-expansion of the type to eliminate now works fine
[helm.git] / components / tactics /
drwxr-xr-x   ..
-rw-r--r-- 11835 .depend
-rw-r--r-- 11835 .depend.opt
-rw-r--r-- 2019 Makefile
-rw-r--r-- 45654 auto.ml
-rw-r--r-- 1406 auto.mli
-rw-r--r-- 4088 autoCache.ml
-rw-r--r-- 1697 autoCache.mli
-rw-r--r-- 12841 autoTactic.ml
-rw-r--r-- 1156 autoTactic.mli
-rw-r--r-- 1637 autoTypes.ml
-rw-r--r-- 1474 autoTypes.mli
-rw-r--r-- 11985 continuationals.ml
-rw-r--r-- 3765 continuationals.mli
-rw-r--r-- 8501 declarative.ml
-rw-r--r-- 2292 declarative.mli
-rw-r--r-- 22027 discriminationTactics.ml
-rw-r--r-- 1288 discriminationTactics.mli
drwxr-xr-x - doc
-rw-r--r-- 6965 eliminationTactics.ml
-rw-r--r-- 1285 eliminationTactics.mli
-rw-r--r-- 17538 equalityTactics.ml
-rw-r--r-- 1695 equalityTactics.mli
-rw-r--r-- 7658 fourier.ml
-rw-r--r-- 1088 fourier.mli
-rw-r--r-- 43459 fourierR.ml
-rw-r--r-- 170 fourierR.mli
-rw-r--r-- 6867 fwdSimplTactic.ml
-rw-r--r-- 1314 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-- 1980 introductionTactics.ml
-rw-r--r-- 1200 introductionTactics.mli
-rw-r--r-- 12688 inversion.ml
-rw-r--r-- 1226 inversion.mli
-rw-r--r-- 7151 inversion_principle.ml
-rw-r--r-- 23 inversion_principle.mli
-rw-r--r-- 18254 metadataQuery.ml
-rw-r--r-- 2326 metadataQuery.mli
-rw-r--r-- 3546 negationTactics.ml
-rw-r--r-- 1094 negationTactics.mli
drwxr-xr-x - paramodulation
-rw-r--r-- 27194 primitiveTactics.ml
-rw-r--r-- 2961 primitiveTactics.mli
-rw-r--r-- 24608 proofEngineHelpers.ml
-rw-r--r-- 4466 proofEngineHelpers.mli
-rw-r--r-- 36378 proofEngineReduction.ml
-rw-r--r-- 1966 proofEngineReduction.mli
-rw-r--r-- 7241 proofEngineStructuralRules.ml
-rw-r--r-- 1423 proofEngineStructuralRules.mli
-rw-r--r-- 3310 proofEngineTypes.ml
-rw-r--r-- 2657 proofEngineTypes.mli
-rw-r--r-- 8529 reductionTactics.ml
-rw-r--r-- 1754 reductionTactics.mli
-rw-r--r-- 22682 ring.ml
-rw-r--r-- 272 ring.mli
-rw-r--r-- 71646 setoids.ml
-rw-r--r-- 2770 setoids.mli
-rw-r--r-- 7106 statefulProofEngine.ml
-rw-r--r-- 4271 statefulProofEngine.mli
-rw-r--r-- 9335 tacticChaser.ml
-rw-r--r-- 12627 tacticals.ml
-rw-r--r-- 2992 tacticals.mli
-rw-r--r-- 3007 tactics.ml
-rw-r--r-- 4088 tactics.mli
-rw-r--r-- 4602 universe.ml
-rw-r--r-- 1648 universe.mli
-rw-r--r-- 7329 variousTactics.ml
-rw-r--r-- 1228 variousTactics.mli