X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Ftest%2Fbasic_1.conf.xml;h=5056ebfbca81c3077d59e8ff6bfc94e94546eb47;hb=da42c465b04bbfc470e73b8060155d1aadd184c5;hp=d9d2d67dcaaf5ef77f8e7dc733f5869b762c9ac3;hpb=2fa001c86e37c76c840122655cb4ffba8bb30cad;p=helm.git diff --git a/matita/components/binaries/matex/test/basic_1.conf.xml b/matita/components/binaries/matex/test/basic_1.conf.xml index d9d2d67dc..5056ebfbc 100644 --- a/matita/components/binaries/matex/test/basic_1.conf.xml +++ b/matita/components/binaries/matex/test/basic_1.conf.xml @@ -1,96 +1,99 @@ +
+ matita.lambdadelta.basic_1 +
- matita.lambdadelta.basic_1.T.defs.B.B.type b I - matita.lambdadelta.basic_1.T.defs.B.B.type ee I - matita.lambdadelta.basic_1.T.defs.B.B.type x I - - matita.lambdadelta.basic_1.T.defs.F.F.type ee I - matita.lambdadelta.basic_1.T.defs.F.F.type f I - matita.lambdadelta.basic_1.T.defs.F.F.type x I - - matita.lambdadelta.basic_1.T.defs.K.K.type e I - matita.lambdadelta.basic_1.T.defs.K.K.type ee I - matita.lambdadelta.basic_1.T.defs.K.K.type k I - matita.lambdadelta.basic_1.T.defs.K.K.type h I - matita.lambdadelta.basic_1.T.defs.K.K.type x I - - matita.lambdadelta.basic_1.C.defs.C.C.type _ X - matita.lambdadelta.basic_1.C.defs.C.C.type a X - matita.lambdadelta.basic_1.C.defs.C.C.type c L - matita.lambdadelta.basic_1.C.defs.C.C.type d L - matita.lambdadelta.basic_1.C.defs.C.C.type e K - matita.lambdadelta.basic_1.C.defs.C.C.type ee X - matita.lambdadelta.basic_1.C.defs.C.C.type x X - matita.lambdadelta.basic_1.C.defs.C.C.type y Y - - matita.lambdadelta.basic_1.T.defs.T.T.type _ X - matita.lambdadelta.basic_1.T.defs.T.T.type e X - matita.lambdadelta.basic_1.T.defs.T.T.type ee X - matita.lambdadelta.basic_1.T.defs.T.T.type t T - matita.lambdadelta.basic_1.T.defs.T.T.type u U - matita.lambdadelta.basic_1.T.defs.T.T.type v V - matita.lambdadelta.basic_1.T.defs.T.T.type w W - matita.lambdadelta.basic_1.T.defs.T.T.type wi W - matita.lambdadelta.basic_1.T.defs.T.T.type x X - matita.lambdadelta.basic_1.T.defs.T.T.type y Y - matita.lambdadelta.basic_1.T.defs.T.T.type z Z - - matita.lambdadelta.basic_1.tlist.defs.TList.TList.type _ Xs - matita.lambdadelta.basic_1.tlist.defs.TList.TList.type e Xs - matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ee Xs - matita.lambdadelta.basic_1.tlist.defs.TList.TList.type t Ts - matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ts Ts - matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ul Us - matita.lambdadelta.basic_1.tlist.defs.TList.TList.type us Us - matita.lambdadelta.basic_1.tlist.defs.TList.TList.type vs Vs - matita.lambdadelta.basic_1.tlist.defs.TList.TList.type ws Ws - matita.lambdadelta.basic_1.tlist.defs.TList.TList.type xs Xs - matita.lambdadelta.basic_1.tlist.defs.TList.TList.type x Xs - matita.lambdadelta.basic_1.tlist.defs.TList.TList.type y Ys - - matita.lambdadelta.basic_1.A.defs.A.A.type _ X - matita.lambdadelta.basic_1.A.defs.A.A.type a A - matita.lambdadelta.basic_1.A.defs.A.A.type b B - matita.lambdadelta.basic_1.A.defs.A.A.type e X - matita.lambdadelta.basic_1.A.defs.A.A.type ee X - matita.lambdadelta.basic_1.A.defs.A.A.type l X - matita.lambdadelta.basic_1.A.defs.A.A.type x X - matita.lambdadelta.basic_1.A.defs.A.A.type y Y - - matita.lambdadelta.basic_1.G.defs.G.G.type g h - - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type _ x - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type d' d - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type d d - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type e e - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type ee e - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type f f - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type g g - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type h h - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type i i - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type j j - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type k k - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type l l - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type m m - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type n n - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type next f - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type v v - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type w w - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type x x - matita.lambdadelta.legacy_1.coq.defs.nat.nat.type y y - - matita.lambdadelta.legacy_1.coq.defs.bool.bool.type b b - matita.lambdadelta.legacy_1.coq.defs.bool.bool.type x x - - matita.lambdadelta.ground_1.plist.defs.PList.PList.type _ f - matita.lambdadelta.ground_1.plist.defs.PList.PList.type e f - matita.lambdadelta.ground_1.plist.defs.PList.PList.type ee f - matita.lambdadelta.ground_1.plist.defs.PList.PList.type hds f - matita.lambdadelta.ground_1.plist.defs.PList.PList.type is f - matita.lambdadelta.ground_1.plist.defs.PList.PList.type p f - matita.lambdadelta.ground_1.plist.defs.PList.PList.type q f - matita.lambdadelta.ground_1.plist.defs.PList.PList.type y f + $(devel.basic1).T.defs.B.B.type b I + $(devel.basic1).T.defs.B.B.type ee I + $(devel.basic1).T.defs.B.B.type x I + + $(devel.basic1).T.defs.F.F.type ee I + $(devel.basic1).T.defs.F.F.type f I + $(devel.basic1).T.defs.F.F.type x I + + $(devel.basic1).T.defs.K.K.type e I + $(devel.basic1).T.defs.K.K.type ee I + $(devel.basic1).T.defs.K.K.type k I + $(devel.basic1).T.defs.K.K.type h I + $(devel.basic1).T.defs.K.K.type x I + + $(devel.basic1).C.defs.C.C.type _ X + $(devel.basic1).C.defs.C.C.type a X + $(devel.basic1).C.defs.C.C.type c L + $(devel.basic1).C.defs.C.C.type d L + $(devel.basic1).C.defs.C.C.type e K + $(devel.basic1).C.defs.C.C.type ee X + $(devel.basic1).C.defs.C.C.type x X + $(devel.basic1).C.defs.C.C.type y Y + + $(devel.basic1).T.defs.T.T.type _ X + $(devel.basic1).T.defs.T.T.type e X + $(devel.basic1).T.defs.T.T.type ee X + $(devel.basic1).T.defs.T.T.type t T + $(devel.basic1).T.defs.T.T.type u U + $(devel.basic1).T.defs.T.T.type v V + $(devel.basic1).T.defs.T.T.type w W + $(devel.basic1).T.defs.T.T.type wi W + $(devel.basic1).T.defs.T.T.type x X + $(devel.basic1).T.defs.T.T.type y Y + $(devel.basic1).T.defs.T.T.type z Z + + $(devel.basic1).tlist.defs.TList.TList.type _ Xs + $(devel.basic1).tlist.defs.TList.TList.type e Xs + $(devel.basic1).tlist.defs.TList.TList.type ee Xs + $(devel.basic1).tlist.defs.TList.TList.type t Ts + $(devel.basic1).tlist.defs.TList.TList.type ts Ts + $(devel.basic1).tlist.defs.TList.TList.type ul Us + $(devel.basic1).tlist.defs.TList.TList.type us Us + $(devel.basic1).tlist.defs.TList.TList.type vs Vs + $(devel.basic1).tlist.defs.TList.TList.type ws Ws + $(devel.basic1).tlist.defs.TList.TList.type xs Xs + $(devel.basic1).tlist.defs.TList.TList.type x Xs + $(devel.basic1).tlist.defs.TList.TList.type y Ys + + $(devel.basic1).A.defs.A.A.type _ X + $(devel.basic1).A.defs.A.A.type a A + $(devel.basic1).A.defs.A.A.type b B + $(devel.basic1).A.defs.A.A.type e X + $(devel.basic1).A.defs.A.A.type ee X + $(devel.basic1).A.defs.A.A.type l X + $(devel.basic1).A.defs.A.A.type x X + $(devel.basic1).A.defs.A.A.type y Y + + $(devel.basic1).G.defs.G.G.type g h + + $(devel.legacy1).coq.defs.nat.nat.type _ x + $(devel.legacy1).coq.defs.nat.nat.type d' d + $(devel.legacy1).coq.defs.nat.nat.type d d + $(devel.legacy1).coq.defs.nat.nat.type e e + $(devel.legacy1).coq.defs.nat.nat.type ee e + $(devel.legacy1).coq.defs.nat.nat.type f f + $(devel.legacy1).coq.defs.nat.nat.type g g + $(devel.legacy1).coq.defs.nat.nat.type h h + $(devel.legacy1).coq.defs.nat.nat.type i i + $(devel.legacy1).coq.defs.nat.nat.type j j + $(devel.legacy1).coq.defs.nat.nat.type k k + $(devel.legacy1).coq.defs.nat.nat.type l l + $(devel.legacy1).coq.defs.nat.nat.type m m + $(devel.legacy1).coq.defs.nat.nat.type n n + $(devel.legacy1).coq.defs.nat.nat.type next f + $(devel.legacy1).coq.defs.nat.nat.type v v + $(devel.legacy1).coq.defs.nat.nat.type w w + $(devel.legacy1).coq.defs.nat.nat.type x x + $(devel.legacy1).coq.defs.nat.nat.type y y + + $(devel.legacy1).coq.defs.bool.bool.type b b + $(devel.legacy1).coq.defs.bool.bool.type x x + + $(devel.ground1).plist.defs.PList.PList.type _ f + $(devel.ground1).plist.defs.PList.PList.type e f + $(devel.ground1).plist.defs.PList.PList.type ee f + $(devel.ground1).plist.defs.PList.PList.type hds f + $(devel.ground1).plist.defs.PList.PList.type is f + $(devel.ground1).plist.defs.PList.PList.type p f + $(devel.ground1).plist.defs.PList.PList.type q f + $(devel.ground1).plist.defs.PList.PList.type y f Prop P R Prop Q R @@ -125,5 +128,149 @@ Prop x H Type[cic:/matita/pts/Type0.univ] f a + + clt_wf__q_ind q_ind_aux + + ex1__leq_sort_SS leq_sort_SS_aux + + flt_wf__q_ind q_ind_aux + + llt_wf__q_ind q_ind_aux + + nf2_gen__nf2_gen_aux nf2_gen_aux + + pc3_ind_left__pc3_left_pc3 pc3_left_pc3_aux + pc3_ind_left__pc3_left_pr3 pc3_left_pr3_aux + pc3_ind_left__pc3_left_sym pc3_left_sym_aux + pc3_ind_left__pc3_left_trans pc3_left_trans_aux + pc3_ind_left__pc3_pc3_left pc3_pc3_left_aux + pc3_wcpr0__pc3_wcpr0_t_aux pc3_wcpr0_t_aux + + pr0_confluence__pr0_cong_delta pr0_cong_delta_aux + pr0_confluence__pr0_cong_upsilon_cong pr0_cong_upsilon_cong_aux + pr0_confluence__pr0_cong_upsilon_delta pr0_cong_upsilon_delta_aux + pr0_confluence__pr0_cong_upsilon_refl pr0_cong_upsilon_refl_aux + pr0_confluence__pr0_cong_upsilon_zeta pr0_cong_upsilon_zeta_aux + pr0_confluence__pr0_delta_delta pr0_delta_delta_aux + pr0_confluence__pr0_delta_tau pr0_delta_tau_aux + pr0_confluence__pr0_upsilon_upsilon pr0_upsilon_upsilon_aux + + pr2_confluence__pr2_delta_delta pr2_delta_delta_aux + pr2_confluence__pr2_free_delta pr2_free_delta_aux + pr2_confluence__pr2_free_free pr2_free_free_aux + + sc3_props__sc3_sn3_abst sc3_sn3_abst_aux + + terms_props__bind_dec bind_dec_aux + terms_props__flat_dec flat_dec_aux + terms_props__kind_dec kind_dec_aux + + tlt_wf__q_ind q_ind_aux + tslt_wf__q_ind q_ind_aux + ty3_nf2_gen__ty3_nf2_inv_abst_aux ty3_nf2_inv_abst_aux +
+
+ + $(devel.basic1).drop1.defs.drop1.drop1.type DropS 2 0 + + $(devel.basic1).drop.defs.drop.drop.type Drop 3 0 + + $(devel.basic1).lift1.defs.lift1.lift1.type FunLiftS 2 0 + $(devel.basic1).lift1.defs.lifts1.lifts1.type FunLiftS 2 0 + + $(devel.basic1).lift.defs.lifts.lifts.type FunLift 3 0 + $(devel.basic1).lift.defs.lift.type FunLift 3 0 + + $(devel.basic1).tlist.defs.TApp.TApp.type RevConsA 2 0 + + $(devel.basic1).tlist.defs.TList.TCons.type ConsA 2 0 +