]> matita.cs.unibo.it Git - helm.git/tree - helm/ocaml/tactics/
Added a filter for uris in tactic "auto".
[helm.git] / helm / ocaml / tactics /
drwxr-xr-x   ..
-rw-r--r-- 59 .cvsignore
-rw-r--r-- 4690 .depend
-rw-r--r-- 727 Makefile
-rw-r--r-- 31596 discriminationTactics.ml
-rw-r--r-- 1220 discriminationTactics.mli
-rw-r--r-- 9174 eliminationTactics.ml
-rw-r--r-- 1345 eliminationTactics.mli
-rw-r--r-- 7039 equalityTactics.ml
-rw-r--r-- 1475 equalityTactics.mli
-rw-r--r-- 2387 filter_auto.ml
-rw-r--r-- 1092 filter_auto.mli
-rw-r--r-- 7658 fourier.ml
-rw-r--r-- 1088 fourier.mli
-rw-r--r-- 43309 fourierR.ml
-rw-r--r-- 170 fourierR.mli
-rw-r--r-- 1748 introductionTactics.ml
-rw-r--r-- 1200 introductionTactics.mli
-rw-r--r-- 7980 match_concl.ml
-rw-r--r-- 1858 match_concl.mli
-rw-r--r-- 2743 negationTactics.ml
-rw-r--r-- 1094 negationTactics.mli
-rw-r--r-- 10356 newConstraints.ml
-rw-r--r-- 2305 newConstraints.mli
-rw-r--r-- 24428 primitiveTactics.ml
-rw-r--r-- 1619 primitiveTactics.mli
-rw-r--r-- 3998 proofEngineHelpers.ml
-rw-r--r-- 1454 proofEngineHelpers.mli
-rw-r--r-- 32268 proofEngineReduction.ml
-rw-r--r-- 1899 proofEngineReduction.mli
-rw-r--r-- 5600 proofEngineStructuralRules.ml
-rw-r--r-- 1109 proofEngineStructuralRules.mli
-rw-r--r-- 1708 proofEngineTypes.ml
-rw-r--r-- 4641 reductionTactics.ml
-rw-r--r-- 1493 reductionTactics.mli
-rw-r--r-- 21015 ring.ml
-rw-r--r-- 272 ring.mli
-rw-r--r-- 8741 statefulProofEngine.ml
-rw-r--r-- 3707 statefulProofEngine.mli
-rw-r--r-- 9841 tacticChaser.ml
-rw-r--r-- 1506 tacticChaser.mli
-rw-r--r-- 7337 tacticals.ml
-rw-r--r-- 1776 tacticals.mli
-rw-r--r-- 7990 variousTactics.ml
-rw-r--r-- 1360 variousTactics.mli