]> matita.cs.unibo.it Git - helm.git/tree - matita/tests/
added a test for the pullback stuff and the possibility to get the coercion graph...
[helm.git] / matita / tests /
drwxr-xr-x   ..
drwxr-xr-x - TPTP
-rw-r--r-- 1327 absurd.ma
-rw-r--r-- 2146 apply.ma
-rw-r--r-- 1214 apply2.ma
-rw-r--r-- 1582 applys.ma
-rw-r--r-- 1586 assumption.ma
drwxr-xr-x - bad_tests
-rw-r--r-- 22813 bool.ma
-rw-r--r-- 1740 change.ma
-rw-r--r-- 1354 clear.ma
-rw-r--r-- 1410 clearbody.ma
-rw-r--r-- 3719 coercions.ma
-rw-r--r-- 1440 comments.ma
-rw-r--r-- 1224 constructor.ma
-rw-r--r-- 2303 continuationals.ma
-rw-r--r-- 1403 contradiction.ma
-rw-r--r-- 1247 cut.ma
-rw-r--r-- 6970 decl.ma
-rw-r--r-- 1375 decompose.ma
-rw-r--r-- 1997 demodulation_coq.ma
-rw-r--r-- 1417 demodulation_matita.ma
-rw-r--r-- 2129 dependent_injection.ma
-rw-r--r-- 2559 discriminate.ma
-rw-r--r-- 2948 elim.ma
-rw-r--r-- 4340 fguidi.ma
-rw-r--r-- 1498 first.ma
-rw-r--r-- 1431 fix_betareduction.ma
-rw-r--r-- 1445 fold.ma
-rw-r--r-- 1832 generalize.ma
-rw-r--r-- 27509 hard_refine.ma
-rw-r--r-- 2131 injection.ma
drwxr-xr-x - interactive
-rw-r--r-- 2126 inversion.ma
-rw-r--r-- 1972 inversion2.ma
-rw-r--r-- 1340 letrec.ma
-rw-r--r-- 977 makefile
-rw-r--r-- 1910 match_inference.ma
-rw-r--r-- 4233 metasenv_ordering.ma
-rw-r--r-- 1104 mysql_escaping.ma
-rw-r--r-- 1778 naiveparamod.ma
-rw-r--r-- 1566 paramodulation.ma
drwxr-xr-x - paramodulation
-rw-r--r-- 2024 pullback.ma
-rw-r--r-- 1723 record.ma
-rw-r--r-- 1898 replace.ma
-rw-r--r-- 2399 rewrite.ma
-rw-r--r-- 1362 second.ma
-rw-r--r-- 1993 simpl.ma
-rw-r--r-- 1336 test2.ma
-rw-r--r-- 1424 test3.ma
-rw-r--r-- 1477 test4.ma
-rw-r--r-- 1368 third.ma
-rw-r--r-- 1632 tinycals.ma
-rw-r--r-- 1752 unfold.ma