From: Enrico Tassi Date: Tue, 27 May 2008 15:42:03 +0000 (+0000) Subject: smarter lexer needed by lambda-delta that is splitting "let rec" statements X-Git-Tag: make_still_working~5119 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d0defade97cf8cf1b5426c73b16b7ea63ccaffbc;p=helm.git smarter lexer needed by lambda-delta that is splitting "let rec" statements on multiple lines --- diff --git a/helm/software/components/content_pres/cicNotationLexer.ml b/helm/software/components/content_pres/cicNotationLexer.ml index bbf7de133..00696cc00 100644 --- a/helm/software/components/content_pres/cicNotationLexer.ml +++ b/helm/software/components/content_pres/cicNotationLexer.ml @@ -50,10 +50,10 @@ let is_ligature_char = true with Not_found -> false)) -let regexp we_proved = "we" ' '+ "proved" -let regexp we_have = "we" ' '+ "have" -let regexp let_rec = "let" ' '+ "rec" -let regexp let_corec = "let" ' '+ "corec" +let regexp we_proved = "we" utf8_blank+ "proved" +let regexp we_have = "we" utf8_blank+ "have" +let regexp let_rec = "let" utf8_blank+ "rec" +let regexp let_corec = "let" utf8_blank+ "corec" let regexp ident_decoration = '\'' | '?' | '`' let regexp ident_cont = ident_letter | xml_digit | '_' let regexp ident = ident_letter ident_cont* ident_decoration* diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/depends b/helm/software/matita/contribs/LAMBDA-TYPES/depends new file mode 100644 index 000000000..cc4ee097b --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/depends @@ -0,0 +1,246 @@ +Legacy-2/preamble.ma Legacy-1/coq/defs.ma Legacy-1/coq/props.ma Legacy-1/definitions.ma Legacy-1/preamble.ma +Legacy-2/coq/defs.ma Legacy-2/preamble.ma +Legacy-2/coq/props.ma Legacy-2/coq/defs.ma +LambdaDelta-1/spare.ma LambdaDelta-1/theory.ma +LambdaDelta-1/preamble.ma Base-1/theory.ma +LambdaDelta-1/theory.ma LambdaDelta-1/csubt/csuba.ma LambdaDelta-1/ex0/props.ma LambdaDelta-1/ex1/props.ma LambdaDelta-1/ex2/props.ma LambdaDelta-1/pr3/wcpr0.ma LambdaDelta-1/sty1/cnt.ma LambdaDelta-1/subst/props.ma LambdaDelta-1/subst0/tlt.ma LambdaDelta-1/ty3/fwd_nf2.ma LambdaDelta-1/ty3/nf2.ma LambdaDelta-1/ty3/sty0.ma LambdaDelta-1/wcpr0/fwd.ma LambdaDelta-1/wf3/props.ma +LambdaDelta-1/definitions.ma LambdaDelta-1/app/defs.ma LambdaDelta-1/aprem/defs.ma LambdaDelta-1/cimp/defs.ma LambdaDelta-1/clen/defs.ma LambdaDelta-1/cnt/defs.ma LambdaDelta-1/csuba/defs.ma LambdaDelta-1/csubc/defs.ma LambdaDelta-1/csubst1/defs.ma LambdaDelta-1/csubt/defs.ma LambdaDelta-1/csubv/defs.ma LambdaDelta-1/ex0/defs.ma LambdaDelta-1/ex1/defs.ma LambdaDelta-1/ex2/defs.ma LambdaDelta-1/flt/defs.ma LambdaDelta-1/fsubst0/defs.ma LambdaDelta-1/iso/defs.ma LambdaDelta-1/llt/defs.ma LambdaDelta-1/next_plus/defs.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pc1/defs.ma LambdaDelta-1/sty1/defs.ma LambdaDelta-1/subst/defs.ma LambdaDelta-1/subst1/defs.ma LambdaDelta-1/tlt/defs.ma LambdaDelta-1/wcpr0/defs.ma LambdaDelta-1/wf3/defs.ma +LambdaDelta-1/csubv/props.ma LambdaDelta-1/T/props.ma LambdaDelta-1/csubv/defs.ma +LambdaDelta-1/csubv/drop.ma LambdaDelta-1/csubv/props.ma LambdaDelta-1/drop/fwd.ma +LambdaDelta-1/csubv/clear.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/csubv/defs.ma +LambdaDelta-1/csubv/getl.ma LambdaDelta-1/csubv/clear.ma LambdaDelta-1/csubv/drop.ma LambdaDelta-1/getl/fwd.ma +LambdaDelta-1/csubv/defs.ma LambdaDelta-1/C/defs.ma +LambdaDelta-1/ex2/props.ma LambdaDelta-1/arity/fwd.ma LambdaDelta-1/ex2/defs.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr2/fwd.ma +LambdaDelta-1/ex2/defs.ma LambdaDelta-1/C/defs.ma +LambdaDelta-1/tlist/props.ma LambdaDelta-1/tlist/defs.ma +LambdaDelta-1/tlist/defs.ma LambdaDelta-1/T/defs.ma +LambdaDelta-1/clen/defs.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/s/defs.ma +LambdaDelta-1/clen/getl.ma LambdaDelta-1/clen/defs.ma LambdaDelta-1/getl/props.ma +LambdaDelta-1/leq/props.ma LambdaDelta-1/aplus/props.ma LambdaDelta-1/leq/fwd.ma +LambdaDelta-1/leq/asucc.ma LambdaDelta-1/leq/props.ma +LambdaDelta-1/leq/defs.ma LambdaDelta-1/aplus/defs.ma +LambdaDelta-1/leq/fwd.ma LambdaDelta-1/leq/defs.ma +LambdaDelta-1/pr3/props.ma LambdaDelta-1/pr1/props.ma LambdaDelta-1/pr2/props.ma LambdaDelta-1/pr3/pr1.ma +LambdaDelta-1/pr3/pr3.ma LambdaDelta-1/pr2/pr2.ma LambdaDelta-1/pr3/props.ma +LambdaDelta-1/pr3/defs.ma LambdaDelta-1/pr2/defs.ma +LambdaDelta-1/pr3/fwd.ma LambdaDelta-1/pr2/fwd.ma LambdaDelta-1/pr3/props.ma +LambdaDelta-1/pr3/subst1.ma LambdaDelta-1/pr2/subst1.ma LambdaDelta-1/pr3/defs.ma +LambdaDelta-1/pr3/iso.ma LambdaDelta-1/iso/props.ma LambdaDelta-1/pr3/fwd.ma LambdaDelta-1/tlist/props.ma +LambdaDelta-1/pr3/wcpr0.ma LambdaDelta-1/pr3/props.ma LambdaDelta-1/wcpr0/getl.ma +LambdaDelta-1/pr3/pr1.ma LambdaDelta-1/pr1/defs.ma LambdaDelta-1/pr3/defs.ma +LambdaDelta-1/ty3/fsubst0.ma LambdaDelta-1/getl/getl.ma LambdaDelta-1/pc3/fsubst0.ma LambdaDelta-1/ty3/props.ma +LambdaDelta-1/ty3/props.ma LambdaDelta-1/pc3/fwd.ma LambdaDelta-1/ty3/fwd.ma +LambdaDelta-1/ty3/arity_props.ma LambdaDelta-1/sc3/arity.ma LambdaDelta-1/ty3/arity.ma +LambdaDelta-1/ty3/arity.ma LambdaDelta-1/arity/pr3.ma LambdaDelta-1/asucc/fwd.ma LambdaDelta-1/ty3/pr3_props.ma +LambdaDelta-1/ty3/pr3_props.ma LambdaDelta-1/ty3/pr3.ma +LambdaDelta-1/ty3/sty0.ma LambdaDelta-1/sty0/fwd.ma LambdaDelta-1/ty3/pr3_props.ma +LambdaDelta-1/ty3/pr3.ma LambdaDelta-1/csubt/ty3.ma LambdaDelta-1/pc1/props.ma LambdaDelta-1/pc3/pc1.ma LambdaDelta-1/pc3/wcpr0.ma LambdaDelta-1/ty3/fsubst0.ma LambdaDelta-1/ty3/subst1.ma +LambdaDelta-1/ty3/defs.ma LambdaDelta-1/G/defs.ma LambdaDelta-1/pc3/defs.ma +LambdaDelta-1/ty3/fwd.ma LambdaDelta-1/pc3/props.ma LambdaDelta-1/ty3/defs.ma +LambdaDelta-1/ty3/dec.ma LambdaDelta-1/getl/dec.ma LambdaDelta-1/getl/flt.ma LambdaDelta-1/pc3/dec.ma +LambdaDelta-1/ty3/subst1.ma LambdaDelta-1/getl/getl.ma LambdaDelta-1/pc3/subst1.ma LambdaDelta-1/ty3/props.ma +LambdaDelta-1/ty3/nf2.ma LambdaDelta-1/nf2/arity.ma LambdaDelta-1/pc3/nf2.ma LambdaDelta-1/ty3/arity.ma +LambdaDelta-1/ty3/fwd_nf2.ma LambdaDelta-1/nf2/fwd.ma LambdaDelta-1/pc3/nf2.ma LambdaDelta-1/ty3/arity_props.ma +LambdaDelta-1/cnt/props.ma LambdaDelta-1/cnt/defs.ma LambdaDelta-1/lift/fwd.ma +LambdaDelta-1/cnt/defs.ma LambdaDelta-1/T/defs.ma +LambdaDelta-1/fsubst0/defs.ma LambdaDelta-1/csubst0/defs.ma +LambdaDelta-1/fsubst0/fwd.ma LambdaDelta-1/fsubst0/defs.ma +LambdaDelta-1/iso/props.ma LambdaDelta-1/iso/fwd.ma +LambdaDelta-1/iso/defs.ma LambdaDelta-1/T/defs.ma +LambdaDelta-1/iso/fwd.ma LambdaDelta-1/iso/defs.ma LambdaDelta-1/tlist/defs.ma +LambdaDelta-1/lift/props.ma LambdaDelta-1/lift/fwd.ma LambdaDelta-1/s/props.ma +LambdaDelta-1/lift/defs.ma LambdaDelta-1/s/defs.ma LambdaDelta-1/tlist/defs.ma +LambdaDelta-1/lift/tlt.ma LambdaDelta-1/lift/fwd.ma LambdaDelta-1/tlt/props.ma +LambdaDelta-1/lift/fwd.ma LambdaDelta-1/lift/defs.ma +LambdaDelta-1/flt/props.ma LambdaDelta-1/C/props.ma LambdaDelta-1/flt/defs.ma +LambdaDelta-1/flt/defs.ma LambdaDelta-1/C/defs.ma +LambdaDelta-1/A/defs.ma LambdaDelta-1/preamble.ma +LambdaDelta-1/subst0/props.ma LambdaDelta-1/subst0/fwd.ma +LambdaDelta-1/subst0/defs.ma LambdaDelta-1/lift/defs.ma +LambdaDelta-1/subst0/tlt.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/lift/tlt.ma LambdaDelta-1/subst0/defs.ma +LambdaDelta-1/subst0/fwd.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/subst0/defs.ma +LambdaDelta-1/subst0/subst0.ma LambdaDelta-1/subst0/props.ma +LambdaDelta-1/subst0/dec.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/subst0/defs.ma +LambdaDelta-1/pr1/props.ma LambdaDelta-1/T/props.ma LambdaDelta-1/pr0/subst1.ma LambdaDelta-1/pr1/defs.ma LambdaDelta-1/subst1/props.ma +LambdaDelta-1/pr1/defs.ma LambdaDelta-1/pr0/defs.ma +LambdaDelta-1/pr1/pr1.ma LambdaDelta-1/pr0/pr0.ma LambdaDelta-1/pr1/props.ma +LambdaDelta-1/T/props.ma LambdaDelta-1/T/defs.ma +LambdaDelta-1/T/defs.ma LambdaDelta-1/preamble.ma +LambdaDelta-1/T/dec.ma LambdaDelta-1/T/defs.ma +LambdaDelta-1/sc3/props.ma LambdaDelta-1/arity/aprem.ma LambdaDelta-1/arity/lift1.ma LambdaDelta-1/csuba/arity.ma LambdaDelta-1/drop1/getl.ma LambdaDelta-1/drop1/props.ma LambdaDelta-1/lift1/props.ma LambdaDelta-1/llt/props.ma LambdaDelta-1/nf2/lift1.ma LambdaDelta-1/sc3/defs.ma LambdaDelta-1/sn3/lift1.ma +LambdaDelta-1/sc3/arity.ma LambdaDelta-1/csubc/arity.ma LambdaDelta-1/csubc/drop1.ma LambdaDelta-1/csubc/getl.ma LambdaDelta-1/csubc/props.ma +LambdaDelta-1/sc3/defs.ma LambdaDelta-1/arity/defs.ma LambdaDelta-1/drop1/defs.ma LambdaDelta-1/sn3/defs.ma +LambdaDelta-1/aplus/props.ma LambdaDelta-1/aplus/defs.ma LambdaDelta-1/next_plus/props.ma +LambdaDelta-1/aplus/defs.ma LambdaDelta-1/asucc/defs.ma +LambdaDelta-1/asucc/defs.ma LambdaDelta-1/A/defs.ma LambdaDelta-1/G/defs.ma +LambdaDelta-1/asucc/fwd.ma LambdaDelta-1/asucc/defs.ma +LambdaDelta-1/aprem/props.ma LambdaDelta-1/aprem/fwd.ma LambdaDelta-1/leq/defs.ma +LambdaDelta-1/aprem/defs.ma LambdaDelta-1/A/defs.ma +LambdaDelta-1/aprem/fwd.ma LambdaDelta-1/aprem/defs.ma +LambdaDelta-1/nf2/props.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr2/fwd.ma +LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr3/pr3.ma +LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr2/defs.ma +LambdaDelta-1/nf2/fwd.ma LambdaDelta-1/T/props.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr2/clen.ma LambdaDelta-1/subst0/dec.ma +LambdaDelta-1/nf2/dec.ma LambdaDelta-1/C/props.ma LambdaDelta-1/nf2/defs.ma LambdaDelta-1/pr0/dec.ma LambdaDelta-1/pr2/clen.ma LambdaDelta-1/pr2/fwd.ma +LambdaDelta-1/nf2/lift1.ma LambdaDelta-1/drop1/fwd.ma LambdaDelta-1/nf2/props.ma +LambdaDelta-1/nf2/iso.ma LambdaDelta-1/iso/props.ma LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/pr3/fwd.ma +LambdaDelta-1/nf2/arity.ma LambdaDelta-1/arity/subst0.ma LambdaDelta-1/nf2/fwd.ma +LambdaDelta-1/drop/props.ma LambdaDelta-1/drop/fwd.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/r/props.ma +LambdaDelta-1/drop/defs.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/lift/defs.ma LambdaDelta-1/r/defs.ma +LambdaDelta-1/drop/fwd.ma LambdaDelta-1/drop/defs.ma +LambdaDelta-1/csuba/drop.ma LambdaDelta-1/csuba/fwd.ma LambdaDelta-1/drop/fwd.ma +LambdaDelta-1/csuba/clear.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/csuba/defs.ma +LambdaDelta-1/csuba/props.ma LambdaDelta-1/csuba/defs.ma +LambdaDelta-1/csuba/arity.ma LambdaDelta-1/arity/props.ma LambdaDelta-1/csuba/getl.ma LambdaDelta-1/csuba/props.ma LambdaDelta-1/csubv/getl.ma +LambdaDelta-1/csuba/defs.ma LambdaDelta-1/arity/defs.ma +LambdaDelta-1/csuba/fwd.ma LambdaDelta-1/csuba/defs.ma +LambdaDelta-1/csuba/getl.ma LambdaDelta-1/csuba/clear.ma LambdaDelta-1/csuba/drop.ma LambdaDelta-1/getl/clear.ma +LambdaDelta-1/C/props.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/T/props.ma +LambdaDelta-1/C/defs.ma LambdaDelta-1/T/defs.ma +LambdaDelta-1/csubt/drop.ma LambdaDelta-1/csubt/fwd.ma LambdaDelta-1/drop/fwd.ma +LambdaDelta-1/csubt/clear.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/csubt/defs.ma +LambdaDelta-1/csubt/props.ma LambdaDelta-1/csubt/defs.ma +LambdaDelta-1/csubt/pc3.ma LambdaDelta-1/csubt/getl.ma LambdaDelta-1/pc3/left.ma +LambdaDelta-1/csubt/defs.ma LambdaDelta-1/ty3/defs.ma +LambdaDelta-1/csubt/fwd.ma LambdaDelta-1/csubt/defs.ma +LambdaDelta-1/csubt/ty3.ma LambdaDelta-1/csubt/pc3.ma LambdaDelta-1/csubt/props.ma +LambdaDelta-1/csubt/getl.ma LambdaDelta-1/csubt/clear.ma LambdaDelta-1/csubt/drop.ma LambdaDelta-1/getl/clear.ma +LambdaDelta-1/csubt/csuba.ma LambdaDelta-1/ty3/arity.ma +LambdaDelta-1/cimp/props.ma LambdaDelta-1/cimp/defs.ma LambdaDelta-1/getl/getl.ma +LambdaDelta-1/cimp/defs.ma LambdaDelta-1/getl/defs.ma +LambdaDelta-1/drop1/props.ma LambdaDelta-1/drop/props.ma LambdaDelta-1/drop1/fwd.ma LambdaDelta-1/getl/defs.ma +LambdaDelta-1/drop1/defs.ma LambdaDelta-1/drop/defs.ma LambdaDelta-1/lift1/defs.ma +LambdaDelta-1/drop1/getl.ma LambdaDelta-1/drop1/fwd.ma LambdaDelta-1/getl/drop.ma +LambdaDelta-1/drop1/fwd.ma LambdaDelta-1/drop1/defs.ma +LambdaDelta-1/lift1/props.ma LambdaDelta-1/drop1/defs.ma LambdaDelta-1/lift/props.ma +LambdaDelta-1/lift1/defs.ma LambdaDelta-1/lift/defs.ma +LambdaDelta-1/lift1/fwd.ma LambdaDelta-1/lift/fwd.ma LambdaDelta-1/lift1/defs.ma +LambdaDelta-1/pr2/pr2.ma LambdaDelta-1/getl/props.ma LambdaDelta-1/pr0/pr0.ma LambdaDelta-1/pr2/defs.ma +LambdaDelta-1/pr2/props.ma LambdaDelta-1/getl/clear.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/pr0/props.ma LambdaDelta-1/pr2/defs.ma +LambdaDelta-1/pr2/defs.ma LambdaDelta-1/getl/defs.ma LambdaDelta-1/pr0/defs.ma +LambdaDelta-1/pr2/fwd.ma LambdaDelta-1/getl/clear.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/pr0/fwd.ma LambdaDelta-1/pr2/defs.ma +LambdaDelta-1/pr2/subst1.ma LambdaDelta-1/csubst1/fwd.ma LambdaDelta-1/csubst1/getl.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/pr0/fwd.ma LambdaDelta-1/pr0/subst1.ma LambdaDelta-1/pr2/defs.ma LambdaDelta-1/subst1/subst1.ma +LambdaDelta-1/pr2/clen.ma LambdaDelta-1/clen/getl.ma LambdaDelta-1/pr2/props.ma +LambdaDelta-1/pc3/fsubst0.ma LambdaDelta-1/csubst0/getl.ma LambdaDelta-1/fsubst0/defs.ma LambdaDelta-1/pc3/left.ma +LambdaDelta-1/pc3/pc1.ma LambdaDelta-1/pc1/defs.ma LambdaDelta-1/pc3/defs.ma LambdaDelta-1/pr3/pr1.ma +LambdaDelta-1/pc3/props.ma LambdaDelta-1/pc3/defs.ma LambdaDelta-1/pr3/pr3.ma +LambdaDelta-1/pc3/left.ma LambdaDelta-1/pc3/props.ma +LambdaDelta-1/pc3/defs.ma LambdaDelta-1/pr3/defs.ma +LambdaDelta-1/pc3/fwd.ma LambdaDelta-1/pc3/props.ma LambdaDelta-1/pr3/fwd.ma +LambdaDelta-1/pc3/dec.ma LambdaDelta-1/nf2/fwd.ma LambdaDelta-1/ty3/arity_props.ma +LambdaDelta-1/pc3/subst1.ma LambdaDelta-1/pc3/props.ma LambdaDelta-1/pr3/subst1.ma +LambdaDelta-1/pc3/wcpr0.ma LambdaDelta-1/pc3/props.ma LambdaDelta-1/wcpr0/getl.ma +LambdaDelta-1/pc3/nf2.ma LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/pc3/defs.ma +LambdaDelta-1/pr0/props.ma LambdaDelta-1/pr0/defs.ma LambdaDelta-1/subst0/subst0.ma +LambdaDelta-1/pr0/pr0.ma LambdaDelta-1/lift/tlt.ma LambdaDelta-1/pr0/fwd.ma +LambdaDelta-1/pr0/defs.ma LambdaDelta-1/subst0/defs.ma +LambdaDelta-1/pr0/fwd.ma LambdaDelta-1/pr0/props.ma +LambdaDelta-1/pr0/dec.ma LambdaDelta-1/T/dec.ma LambdaDelta-1/T/props.ma LambdaDelta-1/pr0/fwd.ma LambdaDelta-1/subst0/dec.ma +LambdaDelta-1/pr0/subst1.ma LambdaDelta-1/pr0/props.ma LambdaDelta-1/subst1/defs.ma +LambdaDelta-1/subst1/props.ma LambdaDelta-1/subst0/props.ma LambdaDelta-1/subst1/defs.ma +LambdaDelta-1/subst1/defs.ma LambdaDelta-1/subst0/defs.ma +LambdaDelta-1/subst1/fwd.ma LambdaDelta-1/subst0/props.ma LambdaDelta-1/subst1/defs.ma +LambdaDelta-1/subst1/subst1.ma LambdaDelta-1/subst0/subst0.ma LambdaDelta-1/subst1/fwd.ma +LambdaDelta-1/tlt/props.ma LambdaDelta-1/tlt/defs.ma +LambdaDelta-1/tlt/defs.ma LambdaDelta-1/T/defs.ma +LambdaDelta-1/ex0/props.ma LambdaDelta-1/aplus/props.ma LambdaDelta-1/ex0/defs.ma LambdaDelta-1/leq/defs.ma +LambdaDelta-1/ex0/defs.ma LambdaDelta-1/A/defs.ma LambdaDelta-1/G/defs.ma +LambdaDelta-1/r/props.ma LambdaDelta-1/r/defs.ma LambdaDelta-1/s/defs.ma +LambdaDelta-1/r/defs.ma LambdaDelta-1/T/defs.ma +LambdaDelta-1/wcpr0/defs.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/pr0/defs.ma +LambdaDelta-1/wcpr0/fwd.ma LambdaDelta-1/wcpr0/defs.ma +LambdaDelta-1/wcpr0/getl.ma LambdaDelta-1/getl/props.ma LambdaDelta-1/wcpr0/defs.ma +LambdaDelta-1/G/defs.ma LambdaDelta-1/preamble.ma +LambdaDelta-1/csubst0/drop.ma LambdaDelta-1/csubst0/fwd.ma LambdaDelta-1/drop/fwd.ma LambdaDelta-1/s/props.ma +LambdaDelta-1/csubst0/clear.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/csubst0/fwd.ma LambdaDelta-1/csubst0/props.ma +LambdaDelta-1/csubst0/props.ma LambdaDelta-1/csubst0/defs.ma +LambdaDelta-1/csubst0/defs.ma LambdaDelta-1/C/defs.ma LambdaDelta-1/subst0/defs.ma +LambdaDelta-1/csubst0/fwd.ma LambdaDelta-1/csubst0/defs.ma +LambdaDelta-1/csubst0/getl.ma LambdaDelta-1/csubst0/clear.ma LambdaDelta-1/csubst0/drop.ma LambdaDelta-1/getl/fwd.ma +LambdaDelta-1/next_plus/props.ma LambdaDelta-1/next_plus/defs.ma +LambdaDelta-1/next_plus/defs.ma LambdaDelta-1/G/defs.ma +LambdaDelta-1/csubc/drop.ma LambdaDelta-1/csubc/fwd.ma LambdaDelta-1/sc3/props.ma +LambdaDelta-1/csubc/clear.ma LambdaDelta-1/csubc/fwd.ma +LambdaDelta-1/csubc/props.ma LambdaDelta-1/csubc/defs.ma LambdaDelta-1/sc3/props.ma +LambdaDelta-1/csubc/arity.ma LambdaDelta-1/csubc/csuba.ma +LambdaDelta-1/csubc/drop1.ma LambdaDelta-1/csubc/drop.ma +LambdaDelta-1/csubc/defs.ma LambdaDelta-1/sc3/defs.ma +LambdaDelta-1/csubc/csuba.ma LambdaDelta-1/csubc/defs.ma LambdaDelta-1/sc3/props.ma +LambdaDelta-1/csubc/getl.ma LambdaDelta-1/csubc/clear.ma LambdaDelta-1/csubc/drop.ma +LambdaDelta-1/csubc/fwd.ma LambdaDelta-1/csubc/defs.ma +LambdaDelta-1/arity/props.ma LambdaDelta-1/arity/fwd.ma +LambdaDelta-1/arity/aprem.ma LambdaDelta-1/aprem/props.ma LambdaDelta-1/arity/cimp.ma LambdaDelta-1/arity/props.ma +LambdaDelta-1/arity/pr3.ma LambdaDelta-1/arity/subst0.ma LambdaDelta-1/csuba/arity.ma LambdaDelta-1/pr0/fwd.ma LambdaDelta-1/pr1/defs.ma LambdaDelta-1/pr3/defs.ma LambdaDelta-1/wcpr0/getl.ma +LambdaDelta-1/arity/defs.ma LambdaDelta-1/getl/defs.ma LambdaDelta-1/leq/defs.ma +LambdaDelta-1/arity/fwd.ma LambdaDelta-1/arity/defs.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/leq/asucc.ma +LambdaDelta-1/arity/subst0.ma LambdaDelta-1/arity/props.ma LambdaDelta-1/csubst0/getl.ma LambdaDelta-1/fsubst0/fwd.ma LambdaDelta-1/getl/getl.ma LambdaDelta-1/subst0/dec.ma LambdaDelta-1/subst0/fwd.ma +LambdaDelta-1/arity/lift1.ma LambdaDelta-1/arity/props.ma LambdaDelta-1/drop1/fwd.ma +LambdaDelta-1/arity/cimp.ma LambdaDelta-1/arity/defs.ma LambdaDelta-1/cimp/props.ma +LambdaDelta-1/subst/props.ma LambdaDelta-1/lift/props.ma LambdaDelta-1/subst/fwd.ma LambdaDelta-1/subst0/defs.ma +LambdaDelta-1/subst/fwd.ma LambdaDelta-1/subst/defs.ma +LambdaDelta-1/subst/defs.ma LambdaDelta-1/lift/defs.ma +LambdaDelta-1/getl/drop.ma LambdaDelta-1/clear/drop.ma LambdaDelta-1/getl/props.ma +LambdaDelta-1/getl/clear.ma LambdaDelta-1/clear/drop.ma LambdaDelta-1/getl/props.ma +LambdaDelta-1/getl/props.ma LambdaDelta-1/clear/props.ma LambdaDelta-1/drop/props.ma LambdaDelta-1/getl/fwd.ma +LambdaDelta-1/getl/defs.ma LambdaDelta-1/clear/defs.ma LambdaDelta-1/drop/defs.ma +LambdaDelta-1/getl/fwd.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/drop/fwd.ma LambdaDelta-1/getl/defs.ma +LambdaDelta-1/getl/dec.ma LambdaDelta-1/getl/props.ma +LambdaDelta-1/getl/flt.ma LambdaDelta-1/clear/props.ma LambdaDelta-1/flt/props.ma LambdaDelta-1/getl/fwd.ma +LambdaDelta-1/getl/getl.ma LambdaDelta-1/getl/clear.ma LambdaDelta-1/getl/drop.ma +LambdaDelta-1/clear/drop.ma LambdaDelta-1/clear/fwd.ma LambdaDelta-1/drop/fwd.ma +LambdaDelta-1/clear/props.ma LambdaDelta-1/clear/fwd.ma +LambdaDelta-1/clear/defs.ma LambdaDelta-1/C/defs.ma +LambdaDelta-1/clear/fwd.ma LambdaDelta-1/clear/defs.ma +LambdaDelta-1/sty1/props.ma LambdaDelta-1/sty0/props.ma LambdaDelta-1/sty1/defs.ma +LambdaDelta-1/sty1/cnt.ma LambdaDelta-1/cnt/props.ma LambdaDelta-1/sty1/props.ma +LambdaDelta-1/sty1/defs.ma LambdaDelta-1/sty0/defs.ma +LambdaDelta-1/s/props.ma LambdaDelta-1/s/defs.ma +LambdaDelta-1/s/defs.ma LambdaDelta-1/T/defs.ma +LambdaDelta-1/pc1/props.ma LambdaDelta-1/pc1/defs.ma LambdaDelta-1/pr1/pr1.ma +LambdaDelta-1/pc1/defs.ma LambdaDelta-1/pr1/defs.ma +LambdaDelta-1/wf3/props.ma LambdaDelta-1/app/defs.ma LambdaDelta-1/wf3/ty3.ma +LambdaDelta-1/wf3/clear.ma LambdaDelta-1/wf3/fwd.ma +LambdaDelta-1/wf3/getl.ma LambdaDelta-1/ty3/dec.ma LambdaDelta-1/wf3/clear.ma +LambdaDelta-1/wf3/ty3.ma LambdaDelta-1/wf3/getl.ma +LambdaDelta-1/wf3/fwd.ma LambdaDelta-1/wf3/defs.ma +LambdaDelta-1/wf3/defs.ma LambdaDelta-1/ty3/defs.ma +LambdaDelta-1/sty0/props.ma LambdaDelta-1/getl/drop.ma LambdaDelta-1/sty0/defs.ma +LambdaDelta-1/sty0/fwd.ma LambdaDelta-1/sty0/defs.ma +LambdaDelta-1/sty0/defs.ma LambdaDelta-1/G/defs.ma LambdaDelta-1/getl/defs.ma +LambdaDelta-1/app/defs.ma LambdaDelta-1/C/defs.ma +LambdaDelta-1/sn3/nf2.ma LambdaDelta-1/nf2/dec.ma LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/sn3/defs.ma +LambdaDelta-1/sn3/props.ma LambdaDelta-1/nf2/iso.ma LambdaDelta-1/pr3/iso.ma LambdaDelta-1/sn3/fwd.ma LambdaDelta-1/sn3/nf2.ma +LambdaDelta-1/sn3/defs.ma LambdaDelta-1/pr3/defs.ma +LambdaDelta-1/sn3/fwd.ma LambdaDelta-1/pr3/props.ma LambdaDelta-1/sn3/defs.ma +LambdaDelta-1/sn3/lift1.ma LambdaDelta-1/drop1/fwd.ma LambdaDelta-1/lift1/fwd.ma LambdaDelta-1/sn3/props.ma +LambdaDelta-1/llt/props.ma LambdaDelta-1/leq/defs.ma LambdaDelta-1/llt/defs.ma +LambdaDelta-1/llt/defs.ma LambdaDelta-1/A/defs.ma +LambdaDelta-1/ex1/props.ma LambdaDelta-1/arity/defs.ma LambdaDelta-1/ex1/defs.ma LambdaDelta-1/leq/props.ma LambdaDelta-1/nf2/pr3.ma LambdaDelta-1/nf2/props.ma LambdaDelta-1/pc3/fwd.ma LambdaDelta-1/ty3/fwd.ma +LambdaDelta-1/ex1/defs.ma LambdaDelta-1/C/defs.ma +LambdaDelta-1/csubst1/props.ma LambdaDelta-1/csubst1/defs.ma LambdaDelta-1/subst1/defs.ma +LambdaDelta-1/csubst1/defs.ma LambdaDelta-1/csubst0/defs.ma +LambdaDelta-1/csubst1/fwd.ma LambdaDelta-1/csubst0/fwd.ma LambdaDelta-1/csubst1/defs.ma LambdaDelta-1/subst1/props.ma +LambdaDelta-1/csubst1/getl.ma LambdaDelta-1/csubst0/getl.ma LambdaDelta-1/csubst1/props.ma LambdaDelta-1/drop/props.ma LambdaDelta-1/subst1/props.ma +Legacy-1/preamble.ma +Legacy-1/spare.ma Legacy-1/theory.ma +Legacy-1/theory.ma Legacy-1/coq/props.ma +Legacy-1/definitions.ma Legacy-1/coq/defs.ma +Legacy-1/coq/props.ma Legacy-1/coq/defs.ma +Legacy-1/coq/defs.ma Legacy-1/preamble.ma +Base-2/preamble.ma Base-1/definitions.ma Legacy-2/theory.ma +Base-1/definitions.ma Base-1/blt/defs.ma Base-1/plist/defs.ma Base-1/types/defs.ma +Base-1/preamble.ma Legacy-1/theory.ma +Base-1/theory.ma Base-1/blt/props.ma Base-1/ext/arith.ma Base-1/ext/tactics.ma Base-1/plist/props.ma Base-1/types/props.ma +Base-1/spare.ma Base-1/theory.ma +Base-1/plist/props.ma Base-1/plist/defs.ma +Base-1/plist/defs.ma Base-1/preamble.ma +Base-1/ext/tactics.ma Base-1/preamble.ma +Base-1/ext/arith.ma Base-1/preamble.ma +Base-1/types/props.ma Base-1/types/defs.ma +Base-1/types/defs.ma Base-1/preamble.ma +Base-1/blt/props.ma Base-1/blt/defs.ma +Base-1/blt/defs.ma Base-1/preamble.ma +Legacy-2/theory.ma +Legacy-2/coq/defs.mma Legacy-2/preamble.ma Legacy-1/coq/defs.ma +Legacy-2/coq/props.mma Legacy-2/preamble.ma Legacy-1/coq/props.ma +Legacy-2/theory.ma Legacy-2/coq/props.ma