X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fpartial.txt;h=1708bccc68a24ea1452919bdeabf928cfad84a61;hb=a40dbe4ef22688b1e9d8b31a7f10150bfc28e111;hp=0ff5a431f69d8c59c70882e24b278f92568c5440;hpb=2f00c2224c66757d00883602cfd0bbd2448eb3ca;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
index 0ff5a431f..1708bccc6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
@@ -1,4 +1,12 @@
-cpxs.ma cpxs_tdeq.ma cpxs_tsts.ma cpxs_tsts_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma
-lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma
-csx.ma csx_simple.ma csx_tsts.ma csx_drops.ma csx_gcp.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma
-csx_vector.ma
+cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_ffdeq.ma cpxs_aaa.ma cpxs_lpx.ma cpxs_cnx.ma cpxs_cpxs.ma
+cpxs_ext.ma
+lpxs.ma lpxs_length.ma lpxs_drops.ma lpxs_lfdeq.ma lpxs_ffdeq.ma lpxs_aaa.ma lpxs_lpx.ma lpxs_cpxs.ma lpxs_lpxs.ma
+csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_fqus.ma csx_lsubr.ma csx_lfdeq.ma csx_ffdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lpx.ma csx_cnx.ma csx_fpbq.ma csx_cpxs.ma csx_lpxs.ma csx_csx.ma
+csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma 
+rdsx.ma rdsx_length.ma rdsx_drops.ma rdsx_fqup.ma rdsx_lpxs.ma rdsx_csx.ma rdsx_rdsx.ma
+lsubsx.ma lsubsx_rdsx.ma lsubsx_lsubsx.ma
+fpbs.ma fpbs_fqup.ma fpbs_fqus.ma fpbs_aaa.ma fpbs_cpx.ma fpbs_fpb.ma fpbs_cpxs.ma fpbs_lpxs.ma fpbs_lpxs.ma fpbs_csx.ma fpbs_fpbs.ma
+fpbg.ma fpbg_fqup.ma fpbg_cpxs.ma fpbg_lpxs.ma fpbg_fpbs.ma fpbg_fpbg.ma
+fsb.ma fsb_ffdeq.ma fsb_aaa.ma fsb_csx.ma fsb_fpbg.ma
+cpms.ma cpms_drops.ma cpms_lsubr.ma cpms_aaa.ma cpms_cpxs.ma
+cprs.ma cprs_drops.ma