X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fbinaries%2Fmatex%2Ftest%2Fbasic_1.conf.xml;h=3d6f14619e3be90231c5695f773ddceb62fd1352;hb=c52e807a10cac88866b61fa458936dc5c0f5ee70;hp=701b0c84ff3f2bff130422721e8096595de3f7e0;hpb=f462726eaf4edb5852851ec5d265cdafe9d3a78d;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 701b0c84f..3d6f14619 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 + $(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 - 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 + $(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 - 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 + $(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 - 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 + $(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 - 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 + $(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 - 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 + $(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 - 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 + $(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 - matita.lambdadelta.basic_1.G.defs.G.G.type g h + $(devel.basic1).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 + $(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 - matita.lambdadelta.legacy_1.coq.defs.bool.bool.type b b - matita.lambdadelta.legacy_1.coq.defs.bool.bool.type x x + $(devel.legacy1).coq.defs.bool.bool.type b b + $(devel.legacy1).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.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 @@ -165,96 +168,96 @@ 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 - + ty3_nf2_inv_abst_premise H_ty3_nf2_inv_abst +
+
+ $(devel.basic1).A.defs.A.AHead.type To 2 0 + $(devel.basic1).A.defs.A.ASort.type AtomB 2 0 + $(devel.basic1).A.fwd.A_rect.A_rect.type APPL 4 0 + $(devel.basic1).aplus.defs.aplus.aplus.type PlusA 3 0 + $(devel.basic1).app.defs.app1.app1.type Shift 2 0 + $(devel.basic1).app.defs.cbk.cbk.type Level 1 0 + $(devel.basic1).aprem.defs.aprem.aprem.type CoPremise 3 0 + $(devel.basic1).arity.defs.arity.arity.type Arity 4 0 + $(devel.basic1).asucc.defs.asucc.asucc.type SuccA 2 0 + $(devel.basic1).C.defs.C.CHead.type LHead 3 0 + $(devel.basic1).C.defs.C.CSort.type AtomA 1 0 + $(devel.basic1).C.defs.cle.type LE 2 0 + $(devel.basic1).C.defs.clt.type LT 2 0 + $(devel.basic1).C.defs.CTail.CTail.type THead 3 0 + $(devel.basic1).C.defs.cweight.cweight.type WeightA 1 0 + $(devel.basic1).C.fwd.C_rect.C_rect.type APPL 4 0 + $(devel.basic1).cimp.defs.cimp.type SubEq 2 0 + $(devel.basic1).clear.defs.clear.clear.type Drop 2 0 + $(devel.basic1).clen.defs.clen.clen.type Length 1 0 + $(devel.basic1).cnt.defs.cnt.cnt.type LEnv 1 0 + $(devel.basic1).csuba.defs.csuba.csuba.type LSupA 3 0 + $(devel.basic1).csubc.defs.csubc.csubc.type LSupC 3 0 + $(devel.basic1).csubst0.defs.csubst0.csubst0.type Subst 4 0 + $(devel.basic1).csubst1.defs.csubst1.csubst1.type SubstS 4 0 + $(devel.basic1).csubt.defs.csubt.csubt.type LSupT 3 0 + $(devel.basic1).csubv.defs.csubv.csubv.type LSup 2 0 + $(devel.basic1).drop1.defs.drop1.drop1.type DropS 3 0 + $(devel.basic1).drop1.defs.ptrans.ptrans.type ApplS 2 0 + $(devel.basic1).drop.defs.drop.drop.type DropB 4 0 + $(devel.basic1).ex0.defs.leqz.leqz.type Equiv 2 0 + $(devel.basic1).flt.defs.flt.type LTB 4 0 + $(devel.basic1).flt.defs.fweight.type WeightB 2 0 + $(devel.basic1).fsubst0.defs.fsubst0.fsubst0.type SubstB 6 0 + $(devel.basic1).G.defs.G.mk_G.type MkSH 2 0 + $(devel.basic1).G.defs.next.next.type Next 2 0 + $(devel.basic1).getl.defs.getl.getl.type DropA 3 0 + $(devel.basic1).iso.defs.iso.iso.type SameTop 2 0 + $(devel.basic1).leq.defs.leq.leq.type EquivA 3 0 + $(devel.basic1).lift1.defs.lift1.lift1.type FunLiftS 2 0 + $(devel.basic1).lift1.defs.lifts1.lifts1.type FunLiftS 2 0 + $(devel.basic1).lift1.defs.trans.trans.type Appl 2 0 + $(devel.basic1).lift.defs.lifts.lifts.type FunLift 3 0 + $(devel.basic1).lift.defs.lift.type FunLift 3 0 + $(devel.basic1).lift.defs.lref_map.lref_map.type FunLift 3 0 + $(devel.basic1).llt.defs.llt.type LT 2 0 + $(devel.basic1).llt.defs.lweight.lweight.type WeightA 1 0 + $(devel.basic1).next_plus.defs.next_plus.next_plus.type NextS 3 0 + $(devel.basic1).nf2.defs.nf2.type RNormal 2 0 + $(devel.basic1).nf2.defs.nfs2.nfs2.type RNormal 2 0 + $(devel.basic1).pc1.defs.pc1.type ConvertS 2 0 + $(devel.basic1).pc3.defs.pc3_left.pc3_left.type CoConvertSA 3 0 + $(devel.basic1).pc3.defs.pc3.type ConvertSA 3 0 + $(devel.basic1).pr0.defs.pr0.pr0.type RStep 2 0 + $(devel.basic1).pr1.defs.pr1.pr1.type RStepS 2 0 + $(devel.basic1).pr2.defs.pr2.pr2.type RStepA 3 0 + $(devel.basic1).pr3.defs.pr3.pr3.type RStepSA 3 0 + $(devel.basic1).r.defs.r.type FunW 2 0 + $(devel.basic1).sc3.defs.sc3.sc3.type RCandidate 4 0 + $(devel.basic1).s.defs.s.type FunV 2 0 + $(devel.basic1).sn3.defs.sn3.sn3.type RStrong 2 0 + $(devel.basic1).sn3.defs.sns3.sns3.type RStrong 2 0 + $(devel.basic1).sty0.defs.sty0.sty0.type TStep 4 0 + $(devel.basic1).sty1.defs.sty1.sty1.type TStepS 4 0 + $(devel.basic1).subst0.defs.subst0.subst0.type Subst 4 0 + $(devel.basic1).subst1.defs.subst1.subst1.type SubstS 4 0 + $(devel.basic1).subst.defs.subst.subst.type FunSubstS 3 0 + $(devel.basic1).T.defs.K.Bind.type Bind 1 0 + $(devel.basic1).T.defs.K.Flat.type Flat 1 0 + $(devel.basic1).T.defs.tle.type LE 2 0 + $(devel.basic1).T.defs.T.THead.type THead 3 0 + $(devel.basic1).T.defs.T.TLRef.type LRef 1 0 + $(devel.basic1).T.defs.T.TSort.type AtomA 1 0 + $(devel.basic1).T.defs.tweight.tweight.type WeightA 1 0 + $(devel.basic1).T.fwd.T_rect.T_rect.type APPL 5 0 + $(devel.basic1).tlist.defs.TApp.TApp.type CoConsA 2 0 + $(devel.basic1).tlist.defs.THeads.THeads.type THead 3 0 + $(devel.basic1).tlist.defs.TList.TCons.type ConsA 2 0 + $(devel.basic1).tlist.defs.tslen.tslen.type Length 1 0 + $(devel.basic1).tlist.defs.tslt.type LT 2 0 + $(devel.basic1).tlt.defs.tlt.type LT 2 0 + $(devel.basic1).tlt.defs.wadd.type CoConsA 2 0 + $(devel.basic1).tlt.defs.weight_map.weight_map.type CoWeightB 2 0 + $(devel.basic1).tlt.defs.weight.type CoWeightA 1 0 + $(devel.basic1).ty3.defs.ty3.ty3.type Type 4 0 + $(devel.basic1).ty3.defs.tys3.tys3.type Type 4 0 + $(devel.basic1).ty3.nf2.ty3_nf2_inv_abst_premise.type APPL 3 0 + $(devel.basic1).wcpr0.defs.wcpr0.wcpr0.type RStep 2 0 + $(devel.basic1).wf3.defs.wf3.wf3.type Valid 3 0
-