]> matita.cs.unibo.it Git - helm.git/tree - helm/gTopLevel/
New: refinement is now used to disambiguate parsing.
[helm.git] / helm / gTopLevel /
drwxr-xr-x   ..
-rw-r--r-- 34 .cvsignore
-rw-r--r-- 5550 .depend
-rw-r--r-- 2927 Makefile
-rw-r--r-- 5074 TATTICHE
-rw-r--r-- 16510 cic2Xml.ml
-rw-r--r-- 1549 cic2Xml.mli
-rw-r--r-- 16333 cic2acic.ml
-rw-r--r-- 2362 cic2acic.mli
-rw-r--r-- 23020 doubleTypeInference.ml
-rw-r--r-- 507 doubleTypeInference.mli
-rw-r--r-- 6822 eliminationTactics.ml
-rw-r--r-- 1118 eliminationTactics.mli
-rw-r--r-- 8760 equalityTactics.ml
-rw-r--r-- 1475 equalityTactics.mli
drwxr-xr-x - esempi
-rw-r--r-- 7658 fourier.ml
-rw-r--r-- 41956 fourierR.ml
-rw-r--r-- 170 fourierR.mli
-rw-r--r-- 121848 gTopLevel.ml
-rw-r--r-- 1790 introductionTactics.ml
-rw-r--r-- 1200 introductionTactics.mli
-rw-r--r-- 3746 logicalOperations.ml
-rw-r--r-- 1210 logicalOperations.mli
-rw-r--r-- 19419 mQueryGenerator.ml
-rw-r--r-- 2495 mQueryGenerator.mli
-rw-r--r-- 6247 mQueryLevels.ml
-rw-r--r-- 1831 mQueryLevels.mli
-rw-r--r-- 7167 mQueryLevels2.ml
-rw-r--r-- 1786 mQueryLevels2.mli
-rw-r--r-- 2452 negationTactics.ml
-rw-r--r-- 1094 negationTactics.mli
-rw-r--r-- 22386 primitiveTactics.ml
-rw-r--r-- 1425 primitiveTactics.mli
-rw-r--r-- 9242 proofEngine.ml
-rw-r--r-- 2791 proofEngine.mli
-rw-r--r-- 4658 proofEngineHelpers.ml
-rw-r--r-- 1800 proofEngineHelpers.mli
-rw-r--r-- 31098 proofEngineReduction.ml
-rw-r--r-- 1819 proofEngineReduction.mli
-rw-r--r-- 5440 proofEngineStructuralRules.ml
-rw-r--r-- 1109 proofEngineStructuralRules.mli
-rw-r--r-- 1513 proofEngineTypes.ml
-rw-r--r-- 4546 reductionTactics.ml
-rw-r--r-- 1469 reductionTactics.mli
-rw-r--r-- 22446 ring.ml
-rw-r--r-- 272 ring.mli
-rw-r--r-- 4297 sequentPp.ml
-rw-r--r-- 1512 sequentPp.mli
-rw-r--r-- 7406 tacticals.ml
-rw-r--r-- 1776 tacticals.mli
drwxr-xr-x - topLevel
-rw-r--r-- 4138 variousTactics.ml
-rw-r--r-- 1229 variousTactics.mli
-rw-r--r-- 2853 xml2Gdome.ml
-rw-r--r-- 1082 xml2Gdome.mli