From 89f42c758bfa3e15324d289774792971f282e684 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 6 May 2009 19:01:31 +0000 Subject: [PATCH] LAMBDA-TYPES: mma's recommitted because inline syntax changed --- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/C/props.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/dec.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/aplus/props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/aprem/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/arity/aprem.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/arity/cimp.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/arity/lift1.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/pr3.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/arity/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/arity/subst0.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/asucc/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/cimp/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/clear/drop.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/clear/props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/clen/getl.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/cnt/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csuba/arity.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csuba/clear.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csuba/drop.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csuba/getl.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csuba/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubc/arity.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubc/clear.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubc/csuba.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop1.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubc/getl.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubc/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/clear.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/drop.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/getl.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/getl.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubt/clear.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubt/csuba.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubt/drop.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubt/getl.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/pc3.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubt/props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/ty3.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubv/clear.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubv/drop.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubv/getl.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/csubv/props.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/drop/props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/drop1/getl.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/drop1/props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/ex0/props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/ex1/props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/ex2/props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/flt/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/fsubst0/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/getl/clear.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/dec.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/drop.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/flt.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/fwd.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/getl.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/getl/props.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/fwd.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/asucc.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/fwd.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/props.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/lift/props.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/tlt.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/lift1/props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/llt/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/next_plus/props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/arity.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/dec.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/fwd.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/iso.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/lift1.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/pr3.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/pc1/props.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/dec.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fsubst0.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fwd.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/left.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/nf2.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/pc1.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/pc3/subst1.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/wcpr0.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/dec.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/fwd.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/pr0.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/pr0/subst1.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/pr1.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/props.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/clen.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/fwd.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/pr2.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/pr2/subst1.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/fwd.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/iso.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr1.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr3.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/pr3/subst1.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/wcpr0.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/r/props.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/s/props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/arity.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/props.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/fwd.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/lift1.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/nf2.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/props.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/sty0/props.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/cnt.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/sty1/props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/subst/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/subst0/dec.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/subst0/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/subst0/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/subst0/subst0.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/subst0/tlt.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/subst1/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/subst1/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/subst1/subst1.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/tlist/props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/tlt/props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity_props.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/dec.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fsubst0.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd_nf2.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/nf2.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3_props.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/props.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/sty0.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/ty3/subst1.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/fwd.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/getl.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/clear.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/fwd.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/getl.mma | 2 +- .../software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/props.mma | 2 +- helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/ty3.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Ground-2/blt/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Ground-2/ext/arith.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Ground-2/ext/tactics.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Ground-2/plist/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Ground-2/types/props.mma | 2 +- .../matita/contribs/LAMBDA-TYPES/Legacy-2/coq/props.mma | 2 +- 168 files changed, 168 insertions(+), 168 deletions(-) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/C/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/C/props.mma index cacddb126..7cbed8e15 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/C/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/C/props.mma @@ -18,5 +18,5 @@ include "Basic-2/C/defs.ma". include "Basic-2/T/props.ma". -inline procedural "Basic-1/C/props.ma". +inline "Basic-1/C/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/dec.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/dec.mma index fc2241b6b..85ff33c1b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/dec.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/dec.mma @@ -16,5 +16,5 @@ include "Basic-2/T/defs.ma". -inline procedural "Basic-1/T/dec.ma". +inline "Basic-1/T/dec.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/props.mma index b55f1b473..58ffc668a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/T/props.mma @@ -16,5 +16,5 @@ include "Basic-2/T/defs.ma". -inline procedural "Basic-1/T/props.ma". +inline "Basic-1/T/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aplus/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aplus/props.mma index 54c23e5cd..9e2234b3b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aplus/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aplus/props.mma @@ -18,5 +18,5 @@ include "Basic-2/aplus/defs.ma". include "Basic-2/next_plus/props.ma". -inline procedural "Basic-1/aplus/props.ma". +inline "Basic-1/aplus/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/fwd.mma index c718804b2..757c62bde 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/aprem/defs.ma". -inline procedural "Basic-1/aprem/fwd.ma". +inline "Basic-1/aprem/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/props.mma index 0f465370c..11509ac4b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/props.mma @@ -18,5 +18,5 @@ include "Basic-2/aprem/fwd.ma". include "Basic-2/leq/defs.ma". -inline procedural "Basic-1/aprem/props.ma". +inline "Basic-1/aprem/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/aprem.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/aprem.mma index fa502573a..7a368efa9 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/aprem.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/aprem.mma @@ -20,5 +20,5 @@ include "Basic-2/arity/cimp.ma". include "Basic-2/aprem/props.ma". -inline procedural "Basic-1/arity/aprem.ma". +inline "Basic-1/arity/aprem.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/cimp.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/cimp.mma index fe0eaa3d7..ca1bf3cad 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/cimp.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/cimp.mma @@ -18,5 +18,5 @@ include "Basic-2/arity/defs.ma". include "Basic-2/cimp/props.ma". -inline procedural "Basic-1/arity/cimp.ma". +inline "Basic-1/arity/cimp.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/fwd.mma index 1f507d36a..7ef60bef2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/fwd.mma @@ -20,5 +20,5 @@ include "Basic-2/leq/asucc.ma". include "Basic-2/getl/drop.ma". -inline procedural "Basic-1/arity/fwd.ma". +inline "Basic-1/arity/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/lift1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/lift1.mma index b3b189574..adde30893 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/lift1.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/lift1.mma @@ -18,5 +18,5 @@ include "Basic-2/arity/props.ma". include "Basic-2/drop1/fwd.ma". -inline procedural "Basic-1/arity/lift1.ma". +inline "Basic-1/arity/lift1.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/pr3.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/pr3.mma index bd9f42ea4..8459c2a35 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/pr3.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/pr3.mma @@ -26,5 +26,5 @@ include "Basic-2/pr0/fwd.ma". include "Basic-2/arity/subst0.ma". -inline procedural "Basic-1/arity/pr3.ma". +inline "Basic-1/arity/pr3.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/props.mma index 4e8db7713..2d5c30d0d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/props.mma @@ -16,5 +16,5 @@ include "Basic-2/arity/fwd.ma". -inline procedural "Basic-1/arity/props.ma". +inline "Basic-1/arity/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/subst0.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/subst0.mma index 38cc5e1dc..ff090fc82 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/subst0.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/arity/subst0.mma @@ -26,5 +26,5 @@ include "Basic-2/subst0/fwd.ma". include "Basic-2/getl/getl.ma". -inline procedural "Basic-1/arity/subst0.ma". +inline "Basic-1/arity/subst0.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/asucc/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/asucc/fwd.mma index 5fcb4195b..d0e22947a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/asucc/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/asucc/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/asucc/defs.ma". -inline procedural "Basic-1/asucc/fwd.ma". +inline "Basic-1/asucc/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/cimp/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/cimp/props.mma index 65d74b41f..288bce2f2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/cimp/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/cimp/props.mma @@ -18,5 +18,5 @@ include "Basic-2/cimp/defs.ma". include "Basic-2/getl/getl.ma". -inline procedural "Basic-1/cimp/props.ma". +inline "Basic-1/cimp/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/drop.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/drop.mma index 67fe50f49..d78b3941a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/drop.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/drop.mma @@ -18,5 +18,5 @@ include "Basic-2/clear/fwd.ma". include "Basic-2/drop/fwd.ma". -inline procedural "Basic-1/clear/drop.ma". +inline "Basic-1/clear/drop.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/fwd.mma index b0262e8a0..e56fb51b1 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/clear/defs.ma". -inline procedural "Basic-1/clear/fwd.ma". +inline "Basic-1/clear/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/props.mma index 58a577666..0bd37aee0 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clear/props.mma @@ -16,5 +16,5 @@ include "Basic-2/clear/fwd.ma". -inline procedural "Basic-1/clear/props.ma". +inline "Basic-1/clear/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clen/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clen/getl.mma index a9d3ff0d9..3d2d8f86c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clen/getl.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/clen/getl.mma @@ -18,5 +18,5 @@ include "Basic-2/clen/defs.ma". include "Basic-2/getl/props.ma". -inline procedural "Basic-1/clen/getl.ma". +inline "Basic-1/clen/getl.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/cnt/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/cnt/props.mma index 62b9e4434..8b288f51f 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/cnt/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/cnt/props.mma @@ -18,5 +18,5 @@ include "Basic-2/cnt/defs.ma". include "Basic-2/lift/fwd.ma". -inline procedural "Basic-1/cnt/props.ma". +inline "Basic-1/cnt/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/arity.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/arity.mma index 369818a18..2d7cdb86d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/arity.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/arity.mma @@ -22,5 +22,5 @@ include "Basic-2/arity/props.ma". include "Basic-2/csubv/getl.ma". -inline procedural "Basic-1/csuba/arity.ma". +inline "Basic-1/csuba/arity.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/clear.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/clear.mma index 0821bfb3f..15098af70 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/clear.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/clear.mma @@ -18,5 +18,5 @@ include "Basic-2/csuba/defs.ma". include "Basic-2/clear/fwd.ma". -inline procedural "Basic-1/csuba/clear.ma". +inline "Basic-1/csuba/clear.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/drop.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/drop.mma index cdd71b487..4aec6957d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/drop.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/drop.mma @@ -18,5 +18,5 @@ include "Basic-2/csuba/fwd.ma". include "Basic-2/drop/fwd.ma". -inline procedural "Basic-1/csuba/drop.ma". +inline "Basic-1/csuba/drop.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/fwd.mma index 743375c8c..2c5a16f23 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/csuba/defs.ma". -inline procedural "Basic-1/csuba/fwd.ma". +inline "Basic-1/csuba/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/getl.mma index 1003ae3ed..e52f58df9 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/getl.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/getl.mma @@ -20,5 +20,5 @@ include "Basic-2/csuba/clear.ma". include "Basic-2/getl/clear.ma". -inline procedural "Basic-1/csuba/getl.ma". +inline "Basic-1/csuba/getl.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/props.mma index b51a48e5a..d1ab31945 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/props.mma @@ -16,5 +16,5 @@ include "Basic-2/csuba/defs.ma". -inline procedural "Basic-1/csuba/props.ma". +inline "Basic-1/csuba/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/arity.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/arity.mma index 672c5c24d..63fff2532 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/arity.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/arity.mma @@ -16,5 +16,5 @@ include "Basic-2/csubc/csuba.ma". -inline procedural "Basic-1/csubc/arity.ma". +inline "Basic-1/csubc/arity.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/clear.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/clear.mma index 8b2b8f4d4..1a0cbcf35 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/clear.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/clear.mma @@ -16,5 +16,5 @@ include "Basic-2/csubc/fwd.ma". -inline procedural "Basic-1/csubc/clear.ma". +inline "Basic-1/csubc/clear.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/csuba.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/csuba.mma index 5c11ce5d0..f3465bf35 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/csuba.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/csuba.mma @@ -18,5 +18,5 @@ include "Basic-2/csubc/defs.ma". include "Basic-2/sc3/props.ma". -inline procedural "Basic-1/csubc/csuba.ma". +inline "Basic-1/csubc/csuba.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop.mma index 358af78fe..2a5d715f5 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop.mma @@ -18,5 +18,5 @@ include "Basic-2/csubc/fwd.ma". include "Basic-2/sc3/props.ma". -inline procedural "Basic-1/csubc/drop.ma". +inline "Basic-1/csubc/drop.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop1.mma index bd910efbe..9863063cf 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop1.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop1.mma @@ -16,5 +16,5 @@ include "Basic-2/csubc/drop.ma". -inline procedural "Basic-1/csubc/drop1.ma". +inline "Basic-1/csubc/drop1.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/fwd.mma index ca11e80ce..1d0dd32ab 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/csubc/defs.ma". -inline procedural "Basic-1/csubc/fwd.ma". +inline "Basic-1/csubc/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/getl.mma index 18370f8cd..60462e153 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/getl.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/getl.mma @@ -18,5 +18,5 @@ include "Basic-2/csubc/drop.ma". include "Basic-2/csubc/clear.ma". -inline procedural "Basic-1/csubc/getl.ma". +inline "Basic-1/csubc/getl.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/props.mma index 8c06dacb9..ff7a8f4e5 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/props.mma @@ -18,5 +18,5 @@ include "Basic-2/csubc/defs.ma". include "Basic-2/sc3/props.ma". -inline procedural "Basic-1/csubc/props.ma". +inline "Basic-1/csubc/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/clear.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/clear.mma index be8bfc196..0b3c214d7 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/clear.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/clear.mma @@ -20,5 +20,5 @@ include "Basic-2/csubst0/fwd.ma". include "Basic-2/clear/fwd.ma". -inline procedural "Basic-1/csubst0/clear.ma". +inline "Basic-1/csubst0/clear.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/drop.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/drop.mma index 90eefc188..8ec4de71c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/drop.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/drop.mma @@ -20,5 +20,5 @@ include "Basic-2/drop/fwd.ma". include "Basic-2/s/props.ma". -inline procedural "Basic-1/csubst0/drop.ma". +inline "Basic-1/csubst0/drop.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/fwd.mma index e44c4945f..85ddb329e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/csubst0/defs.ma". -inline procedural "Basic-1/csubst0/fwd.ma". +inline "Basic-1/csubst0/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/getl.mma index b2deae890..679c49e9e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/getl.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/getl.mma @@ -20,5 +20,5 @@ include "Basic-2/csubst0/drop.ma". include "Basic-2/getl/fwd.ma". -inline procedural "Basic-1/csubst0/getl.ma". +inline "Basic-1/csubst0/getl.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/props.mma index f5af7cd64..fee62c651 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/props.mma @@ -16,5 +16,5 @@ include "Basic-2/csubst0/defs.ma". -inline procedural "Basic-1/csubst0/props.ma". +inline "Basic-1/csubst0/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/fwd.mma index b09e92f45..2c9d5bedb 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/fwd.mma @@ -20,5 +20,5 @@ include "Basic-2/csubst0/fwd.ma". include "Basic-2/subst1/props.ma". -inline procedural "Basic-1/csubst1/fwd.ma". +inline "Basic-1/csubst1/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/getl.mma index 92e622951..05b80d444 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/getl.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/getl.mma @@ -22,5 +22,5 @@ include "Basic-2/subst1/props.ma". include "Basic-2/drop/props.ma". -inline procedural "Basic-1/csubst1/getl.ma". +inline "Basic-1/csubst1/getl.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/props.mma index ca8d9969c..7480c122d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/props.mma @@ -18,5 +18,5 @@ include "Basic-2/csubst1/defs.ma". include "Basic-2/subst1/defs.ma". -inline procedural "Basic-1/csubst1/props.ma". +inline "Basic-1/csubst1/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/clear.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/clear.mma index 2502280a8..c35e253b4 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/clear.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/clear.mma @@ -18,5 +18,5 @@ include "Basic-2/csubt/defs.ma". include "Basic-2/clear/fwd.ma". -inline procedural "Basic-1/csubt/clear.ma". +inline "Basic-1/csubt/clear.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/csuba.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/csuba.mma index 3aee698d6..3145d010e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/csuba.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/csuba.mma @@ -16,5 +16,5 @@ include "Basic-2/ty3/arity.ma". -inline procedural "Basic-1/csubt/csuba.ma". +inline "Basic-1/csubt/csuba.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/drop.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/drop.mma index 610073d97..7d8d90b33 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/drop.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/drop.mma @@ -18,5 +18,5 @@ include "Basic-2/csubt/fwd.ma". include "Basic-2/drop/fwd.ma". -inline procedural "Basic-1/csubt/drop.ma". +inline "Basic-1/csubt/drop.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/fwd.mma index 3cdde9d71..195de62cb 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/csubt/defs.ma". -inline procedural "Basic-1/csubt/fwd.ma". +inline "Basic-1/csubt/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/getl.mma index e7d81a5e9..14299efa2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/getl.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/getl.mma @@ -20,5 +20,5 @@ include "Basic-2/csubt/drop.ma". include "Basic-2/getl/clear.ma". -inline procedural "Basic-1/csubt/getl.ma". +inline "Basic-1/csubt/getl.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/pc3.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/pc3.mma index a6d7a967d..48152a367 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/pc3.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/pc3.mma @@ -18,5 +18,5 @@ include "Basic-2/csubt/getl.ma". include "Basic-2/pc3/left.ma". -inline procedural "Basic-1/csubt/pc3.ma". +inline "Basic-1/csubt/pc3.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/props.mma index a663399b7..59d3c5188 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/props.mma @@ -16,5 +16,5 @@ include "Basic-2/csubt/defs.ma". -inline procedural "Basic-1/csubt/props.ma". +inline "Basic-1/csubt/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/ty3.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/ty3.mma index ee9e065c1..8bb74616a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/ty3.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/ty3.mma @@ -18,5 +18,5 @@ include "Basic-2/csubt/pc3.ma". include "Basic-2/csubt/props.ma". -inline procedural "Basic-1/csubt/ty3.ma". +inline "Basic-1/csubt/ty3.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/clear.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/clear.mma index cb374edc1..77768e993 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/clear.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/clear.mma @@ -18,5 +18,5 @@ include "Basic-2/csubv/defs.ma". include "Basic-2/clear/fwd.ma". -inline procedural "Basic-1/csubv/clear.ma". +inline "Basic-1/csubv/clear.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/drop.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/drop.mma index 9dfe7cca0..d0d2b3f76 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/drop.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/drop.mma @@ -18,5 +18,5 @@ include "Basic-2/csubv/props.ma". include "Basic-2/drop/fwd.ma". -inline procedural "Basic-1/csubv/drop.ma". +inline "Basic-1/csubv/drop.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/getl.mma index a9e95aad4..66c63a639 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/getl.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/getl.mma @@ -20,5 +20,5 @@ include "Basic-2/csubv/drop.ma". include "Basic-2/getl/fwd.ma". -inline procedural "Basic-1/csubv/getl.ma". +inline "Basic-1/csubv/getl.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/props.mma index 13fae5503..44d2edf27 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/props.mma @@ -18,5 +18,5 @@ include "Basic-2/csubv/defs.ma". include "Basic-2/T/props.ma". -inline procedural "Basic-1/csubv/props.ma". +inline "Basic-1/csubv/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/fwd.mma index 1e889f6ff..d88936b9c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/drop/defs.ma". -inline procedural "Basic-1/drop/fwd.ma". +inline "Basic-1/drop/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/props.mma index b21052d8f..9af06df85 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop/props.mma @@ -20,5 +20,5 @@ include "Basic-2/lift/props.ma". include "Basic-2/r/props.ma". -inline procedural "Basic-1/drop/props.ma". +inline "Basic-1/drop/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/fwd.mma index 771733bbc..78b91b349 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/drop1/defs.ma". -inline procedural "Basic-1/drop1/fwd.ma". +inline "Basic-1/drop1/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/getl.mma index b8856b912..0b9e358d2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/getl.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/getl.mma @@ -18,5 +18,5 @@ include "Basic-2/drop1/fwd.ma". include "Basic-2/getl/drop.ma". -inline procedural "Basic-1/drop1/getl.ma". +inline "Basic-1/drop1/getl.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/props.mma index 18a856e8a..f4f2204ac 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/props.mma @@ -20,5 +20,5 @@ include "Basic-2/drop/props.ma". include "Basic-2/getl/defs.ma". -inline procedural "Basic-1/drop1/props.ma". +inline "Basic-1/drop1/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex0/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex0/props.mma index 8680a106f..80204275f 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex0/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex0/props.mma @@ -20,5 +20,5 @@ include "Basic-2/leq/defs.ma". include "Basic-2/aplus/props.ma". -inline procedural "Basic-1/ex0/props.ma". +inline "Basic-1/ex0/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex1/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex1/props.mma index efc47ad2a..8ec7ebe3e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex1/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex1/props.mma @@ -28,5 +28,5 @@ include "Basic-2/arity/defs.ma". include "Basic-2/leq/props.ma". -inline procedural "Basic-1/ex1/props.ma". +inline "Basic-1/ex1/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex2/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex2/props.mma index 44299ae27..56d0d8557 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex2/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ex2/props.mma @@ -22,5 +22,5 @@ include "Basic-2/pr2/fwd.ma". include "Basic-2/arity/fwd.ma". -inline procedural "Basic-1/ex2/props.ma". +inline "Basic-1/ex2/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/flt/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/flt/props.mma index 81509432b..e5b76348f 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/flt/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/flt/props.mma @@ -18,5 +18,5 @@ include "Basic-2/flt/defs.ma". include "Basic-2/C/props.ma". -inline procedural "Basic-1/flt/props.ma". +inline "Basic-1/flt/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/fsubst0/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/fsubst0/fwd.mma index e04ab42fe..4a60d7191 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/fsubst0/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/fsubst0/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/fsubst0/defs.ma". -inline procedural "Basic-1/fsubst0/fwd.ma". +inline "Basic-1/fsubst0/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/clear.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/clear.mma index 4a94110dc..3f69bde5d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/clear.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/clear.mma @@ -18,5 +18,5 @@ include "Basic-2/getl/props.ma". include "Basic-2/clear/drop.ma". -inline procedural "Basic-1/getl/clear.ma". +inline "Basic-1/getl/clear.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/dec.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/dec.mma index 8be561b34..4085b140e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/dec.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/dec.mma @@ -16,5 +16,5 @@ include "Basic-2/getl/props.ma". -inline procedural "Basic-1/getl/dec.ma". +inline "Basic-1/getl/dec.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/drop.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/drop.mma index 519905e39..ff4bb646f 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/drop.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/drop.mma @@ -18,5 +18,5 @@ include "Basic-2/getl/props.ma". include "Basic-2/clear/drop.ma". -inline procedural "Basic-1/getl/drop.ma". +inline "Basic-1/getl/drop.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/flt.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/flt.mma index 7e96ea75f..c030693f5 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/flt.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/flt.mma @@ -20,5 +20,5 @@ include "Basic-2/clear/props.ma". include "Basic-2/flt/props.ma". -inline procedural "Basic-1/getl/flt.ma". +inline "Basic-1/getl/flt.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/fwd.mma index 09e904984..dfcee9576 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/fwd.mma @@ -20,5 +20,5 @@ include "Basic-2/drop/fwd.ma". include "Basic-2/clear/fwd.ma". -inline procedural "Basic-1/getl/fwd.ma". +inline "Basic-1/getl/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/getl.mma index 2bbee600a..b5e5163d7 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/getl.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/getl.mma @@ -18,5 +18,5 @@ include "Basic-2/getl/drop.ma". include "Basic-2/getl/clear.ma". -inline procedural "Basic-1/getl/getl.ma". +inline "Basic-1/getl/getl.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/props.mma index 65e4f5922..00ff97539 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/getl/props.mma @@ -20,5 +20,5 @@ include "Basic-2/drop/props.ma". include "Basic-2/clear/props.ma". -inline procedural "Basic-1/getl/props.ma". +inline "Basic-1/getl/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/fwd.mma index b23bf49ef..8ae8aaad1 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/fwd.mma @@ -18,5 +18,5 @@ include "Basic-2/iso/defs.ma". include "Basic-2/tlist/defs.ma". -inline procedural "Basic-1/iso/fwd.ma". +inline "Basic-1/iso/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/props.mma index f800970b2..c689ea1fc 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/iso/props.mma @@ -16,5 +16,5 @@ include "Basic-2/iso/fwd.ma". -inline procedural "Basic-1/iso/props.ma". +inline "Basic-1/iso/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/asucc.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/asucc.mma index 8465e224c..a89191b08 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/asucc.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/asucc.mma @@ -16,5 +16,5 @@ include "Basic-2/leq/props.ma". -inline procedural "Basic-1/leq/asucc.ma". +inline "Basic-1/leq/asucc.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/fwd.mma index b390962ac..750437135 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/leq/defs.ma". -inline procedural "Basic-1/leq/fwd.ma". +inline "Basic-1/leq/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/props.mma index 780abb9fc..b2509dd31 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/leq/props.mma @@ -18,5 +18,5 @@ include "Basic-2/leq/fwd.ma". include "Basic-2/aplus/props.ma". -inline procedural "Basic-1/leq/props.ma". +inline "Basic-1/leq/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/fwd.mma index 9111d87fc..95a454dbe 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/lift/defs.ma". -inline procedural "Basic-1/lift/fwd.ma". +inline "Basic-1/lift/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/props.mma index dee77c3f8..88f85f5cb 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/props.mma @@ -18,5 +18,5 @@ include "Basic-2/lift/fwd.ma". include "Basic-2/s/props.ma". -inline procedural "Basic-1/lift/props.ma". +inline "Basic-1/lift/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/tlt.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/tlt.mma index ee45a4799..51c972987 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/tlt.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift/tlt.mma @@ -18,5 +18,5 @@ include "Basic-2/lift/fwd.ma". include "Basic-2/tlt/props.ma". -inline procedural "Basic-1/lift/tlt.ma". +inline "Basic-1/lift/tlt.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/fwd.mma index d2823197e..3aabe676f 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/fwd.mma @@ -18,5 +18,5 @@ include "Basic-2/lift1/defs.ma". include "Basic-2/lift/fwd.ma". -inline procedural "Basic-1/lift1/fwd.ma". +inline "Basic-1/lift1/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/props.mma index 7e5f7f7a1..89bed2166 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/props.mma @@ -18,5 +18,5 @@ include "Basic-2/lift/props.ma". include "Basic-2/drop1/defs.ma". -inline procedural "Basic-1/lift1/props.ma". +inline "Basic-1/lift1/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/llt/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/llt/props.mma index 505fdd567..462e5c575 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/llt/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/llt/props.mma @@ -18,5 +18,5 @@ include "Basic-2/llt/defs.ma". include "Basic-2/leq/defs.ma". -inline procedural "Basic-1/llt/props.ma". +inline "Basic-1/llt/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/next_plus/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/next_plus/props.mma index e08bd778d..8e6ff559c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/next_plus/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/next_plus/props.mma @@ -16,5 +16,5 @@ include "Basic-2/next_plus/defs.ma". -inline procedural "Basic-1/next_plus/props.ma". +inline "Basic-1/next_plus/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/arity.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/arity.mma index 24a7f1b46..356dfa591 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/arity.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/arity.mma @@ -18,5 +18,5 @@ include "Basic-2/nf2/fwd.ma". include "Basic-2/arity/subst0.ma". -inline procedural "Basic-1/nf2/arity.ma". +inline "Basic-1/nf2/arity.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/dec.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/dec.mma index ca725c3ae..179da42ff 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/dec.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/dec.mma @@ -24,5 +24,5 @@ include "Basic-2/pr0/dec.ma". include "Basic-2/C/props.ma". -inline procedural "Basic-1/nf2/dec.ma". +inline "Basic-1/nf2/dec.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/fwd.mma index 43248cca2..0f941386e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/fwd.mma @@ -22,5 +22,5 @@ include "Basic-2/subst0/dec.ma". include "Basic-2/T/props.ma". -inline procedural "Basic-1/nf2/fwd.ma". +inline "Basic-1/nf2/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/iso.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/iso.mma index b52c08cb7..0c6309e1c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/iso.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/iso.mma @@ -20,5 +20,5 @@ include "Basic-2/pr3/fwd.ma". include "Basic-2/iso/props.ma". -inline procedural "Basic-1/nf2/iso.ma". +inline "Basic-1/nf2/iso.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/lift1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/lift1.mma index 8291013c6..250c8dd78 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/lift1.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/lift1.mma @@ -18,5 +18,5 @@ include "Basic-2/nf2/props.ma". include "Basic-2/drop1/fwd.ma". -inline procedural "Basic-1/nf2/lift1.ma". +inline "Basic-1/nf2/lift1.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/pr3.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/pr3.mma index 7b5a3b036..00ba3ffab 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/pr3.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/pr3.mma @@ -18,5 +18,5 @@ include "Basic-2/nf2/defs.ma". include "Basic-2/pr3/pr3.ma". -inline procedural "Basic-1/nf2/pr3.ma". +inline "Basic-1/nf2/pr3.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/props.mma index 565a5316b..6977bd069 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/props.mma @@ -18,5 +18,5 @@ include "Basic-2/nf2/defs.ma". include "Basic-2/pr2/fwd.ma". -inline procedural "Basic-1/nf2/props.ma". +inline "Basic-1/nf2/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc1/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc1/props.mma index a73cc0a9d..f031a2362 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc1/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc1/props.mma @@ -18,5 +18,5 @@ include "Basic-2/pc1/defs.ma". include "Basic-2/pr1/pr1.ma". -inline procedural "Basic-1/pc1/props.ma". +inline "Basic-1/pc1/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/dec.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/dec.mma index b8455a117..d5ed4097b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/dec.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/dec.mma @@ -18,5 +18,5 @@ include "Basic-2/ty3/arity_props.ma". include "Basic-2/nf2/fwd.ma". -inline procedural "Basic-1/pc3/dec.ma". +inline "Basic-1/pc3/dec.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fsubst0.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fsubst0.mma index ceb6970c1..478c285af 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fsubst0.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fsubst0.mma @@ -20,5 +20,5 @@ include "Basic-2/fsubst0/defs.ma". include "Basic-2/csubst0/getl.ma". -inline procedural "Basic-1/pc3/fsubst0.ma". +inline "Basic-1/pc3/fsubst0.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fwd.mma index e547cb96e..83816ceac 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fwd.mma @@ -18,5 +18,5 @@ include "Basic-2/pc3/props.ma". include "Basic-2/pr3/fwd.ma". -inline procedural "Basic-1/pc3/fwd.ma". +inline "Basic-1/pc3/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/left.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/left.mma index 9be44a05b..a0102b201 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/left.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/left.mma @@ -16,5 +16,5 @@ include "Basic-2/pc3/props.ma". -inline procedural "Basic-1/pc3/left.ma". +inline "Basic-1/pc3/left.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/nf2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/nf2.mma index d3db0ecee..38a00ff31 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/nf2.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/nf2.mma @@ -18,5 +18,5 @@ include "Basic-2/pc3/defs.ma". include "Basic-2/nf2/pr3.ma". -inline procedural "Basic-1/pc3/nf2.ma". +inline "Basic-1/pc3/nf2.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/pc1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/pc1.mma index 35376ac79..0a82a8adc 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/pc1.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/pc1.mma @@ -20,5 +20,5 @@ include "Basic-2/pc1/defs.ma". include "Basic-2/pr3/pr1.ma". -inline procedural "Basic-1/pc3/pc1.ma". +inline "Basic-1/pc3/pc1.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/props.mma index 36c526b0a..01c5ee4e8 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/props.mma @@ -18,5 +18,5 @@ include "Basic-2/pc3/defs.ma". include "Basic-2/pr3/pr3.ma". -inline procedural "Basic-1/pc3/props.ma". +inline "Basic-1/pc3/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/subst1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/subst1.mma index 8f00fb8e6..1ec4a10d5 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/subst1.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/subst1.mma @@ -18,5 +18,5 @@ include "Basic-2/pc3/props.ma". include "Basic-2/pr3/subst1.ma". -inline procedural "Basic-1/pc3/subst1.ma". +inline "Basic-1/pc3/subst1.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/wcpr0.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/wcpr0.mma index 5b99aa516..98ae77c9b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/wcpr0.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/wcpr0.mma @@ -18,5 +18,5 @@ include "Basic-2/pc3/props.ma". include "Basic-2/wcpr0/getl.ma". -inline procedural "Basic-1/pc3/wcpr0.ma". +inline "Basic-1/pc3/wcpr0.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/dec.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/dec.mma index ce38c93bb..c88b2b725 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/dec.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/dec.mma @@ -22,5 +22,5 @@ include "Basic-2/T/dec.ma". include "Basic-2/T/props.ma". -inline procedural "Basic-1/pr0/dec.ma". +inline "Basic-1/pr0/dec.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/fwd.mma index 7932cb99d..2349a5127 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/pr0/props.ma". -inline procedural "Basic-1/pr0/fwd.ma". +inline "Basic-1/pr0/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/pr0.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/pr0.mma index 8021fe15f..cc88c47e0 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/pr0.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/pr0.mma @@ -18,5 +18,5 @@ include "Basic-2/pr0/fwd.ma". include "Basic-2/lift/tlt.ma". -inline procedural "Basic-1/pr0/pr0.ma". +inline "Basic-1/pr0/pr0.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/props.mma index 7cb130986..9b8e83a73 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/props.mma @@ -18,5 +18,5 @@ include "Basic-2/pr0/defs.ma". include "Basic-2/subst0/subst0.ma". -inline procedural "Basic-1/pr0/props.ma". +inline "Basic-1/pr0/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/subst1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/subst1.mma index 62f059201..a4af1a695 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/subst1.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/subst1.mma @@ -18,5 +18,5 @@ include "Basic-2/pr0/props.ma". include "Basic-2/subst1/defs.ma". -inline procedural "Basic-1/pr0/subst1.ma". +inline "Basic-1/pr0/subst1.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/pr1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/pr1.mma index e94793c50..f05ca1cd3 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/pr1.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/pr1.mma @@ -18,5 +18,5 @@ include "Basic-2/pr1/props.ma". include "Basic-2/pr0/pr0.ma". -inline procedural "Basic-1/pr1/pr1.ma". +inline "Basic-1/pr1/pr1.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/props.mma index 59da19ba9..5ec9c7f3e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/props.mma @@ -22,5 +22,5 @@ include "Basic-2/subst1/props.ma". include "Basic-2/T/props.ma". -inline procedural "Basic-1/pr1/props.ma". +inline "Basic-1/pr1/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/clen.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/clen.mma index 86b48b799..e3ea2f078 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/clen.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/clen.mma @@ -18,5 +18,5 @@ include "Basic-2/pr2/props.ma". include "Basic-2/clen/getl.ma". -inline procedural "Basic-1/pr2/clen.ma". +inline "Basic-1/pr2/clen.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/fwd.mma index 5aaaa6b34..9ec452e99 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/fwd.mma @@ -22,5 +22,5 @@ include "Basic-2/getl/drop.ma". include "Basic-2/getl/clear.ma". -inline procedural "Basic-1/pr2/fwd.ma". +inline "Basic-1/pr2/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/pr2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/pr2.mma index f2a692665..8879c71e8 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/pr2.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/pr2.mma @@ -20,5 +20,5 @@ include "Basic-2/pr0/pr0.ma". include "Basic-2/getl/props.ma". -inline procedural "Basic-1/pr2/pr2.ma". +inline "Basic-1/pr2/pr2.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/props.mma index 7db1b656a..b0e27c8fc 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/props.mma @@ -22,5 +22,5 @@ include "Basic-2/getl/drop.ma". include "Basic-2/getl/clear.ma". -inline procedural "Basic-1/pr2/props.ma". +inline "Basic-1/pr2/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/subst1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/subst1.mma index b0c47c4a3..61b161222 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/subst1.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/subst1.mma @@ -28,5 +28,5 @@ include "Basic-2/subst1/subst1.ma". include "Basic-2/getl/drop.ma". -inline procedural "Basic-1/pr2/subst1.ma". +inline "Basic-1/pr2/subst1.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/fwd.mma index 9445d5d1d..a29ddcee0 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/fwd.mma @@ -18,5 +18,5 @@ include "Basic-2/pr3/props.ma". include "Basic-2/pr2/fwd.ma". -inline procedural "Basic-1/pr3/fwd.ma". +inline "Basic-1/pr3/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/iso.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/iso.mma index 91b74af6c..a401d94dc 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/iso.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/iso.mma @@ -20,5 +20,5 @@ include "Basic-2/iso/props.ma". include "Basic-2/tlist/props.ma". -inline procedural "Basic-1/pr3/iso.ma". +inline "Basic-1/pr3/iso.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr1.mma index 31599c3c9..6827dfddc 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr1.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr1.mma @@ -18,5 +18,5 @@ include "Basic-2/pr3/defs.ma". include "Basic-2/pr1/defs.ma". -inline procedural "Basic-1/pr3/pr1.ma". +inline "Basic-1/pr3/pr1.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr3.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr3.mma index 866281845..a393080b6 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr3.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr3.mma @@ -18,5 +18,5 @@ include "Basic-2/pr3/props.ma". include "Basic-2/pr2/pr2.ma". -inline procedural "Basic-1/pr3/pr3.ma". +inline "Basic-1/pr3/pr3.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/props.mma index 055cd0b15..c87af259a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/props.mma @@ -20,5 +20,5 @@ include "Basic-2/pr2/props.ma". include "Basic-2/pr1/props.ma". -inline procedural "Basic-1/pr3/props.ma". +inline "Basic-1/pr3/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/subst1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/subst1.mma index bb74e3f7d..73288e883 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/subst1.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/subst1.mma @@ -18,5 +18,5 @@ include "Basic-2/pr3/defs.ma". include "Basic-2/pr2/subst1.ma". -inline procedural "Basic-1/pr3/subst1.ma". +inline "Basic-1/pr3/subst1.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/wcpr0.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/wcpr0.mma index 09a0b32ff..6c30039f1 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/wcpr0.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/wcpr0.mma @@ -18,5 +18,5 @@ include "Basic-2/pr3/props.ma". include "Basic-2/wcpr0/getl.ma". -inline procedural "Basic-1/pr3/wcpr0.ma". +inline "Basic-1/pr3/wcpr0.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/r/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/r/props.mma index 1cee8e5f6..79edc95f4 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/r/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/r/props.mma @@ -18,5 +18,5 @@ include "Basic-2/r/defs.ma". include "Basic-2/s/defs.ma". -inline procedural "Basic-1/r/props.ma". +inline "Basic-1/r/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/s/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/s/props.mma index e77078ec5..35f1ad31b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/s/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/s/props.mma @@ -16,5 +16,5 @@ include "Basic-2/s/defs.ma". -inline procedural "Basic-1/s/props.ma". +inline "Basic-1/s/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/arity.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/arity.mma index 6d498e3c9..9fa3eaf93 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/arity.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/arity.mma @@ -22,5 +22,5 @@ include "Basic-2/csubc/drop1.ma". include "Basic-2/csubc/props.ma". -inline procedural "Basic-1/sc3/arity.ma". +inline "Basic-1/sc3/arity.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/props.mma index 2a7989263..859458266 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/props.mma @@ -34,5 +34,5 @@ include "Basic-2/drop1/props.ma". include "Basic-2/lift1/props.ma". -inline procedural "Basic-1/sc3/props.ma". +inline "Basic-1/sc3/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/fwd.mma index 92427e1cd..a4662eefa 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/fwd.mma @@ -18,5 +18,5 @@ include "Basic-2/sn3/defs.ma". include "Basic-2/pr3/props.ma". -inline procedural "Basic-1/sn3/fwd.ma". +inline "Basic-1/sn3/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/lift1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/lift1.mma index 9839254a9..e8c0c4de2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/lift1.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/lift1.mma @@ -20,5 +20,5 @@ include "Basic-2/drop1/fwd.ma". include "Basic-2/lift1/fwd.ma". -inline procedural "Basic-1/sn3/lift1.ma". +inline "Basic-1/sn3/lift1.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/nf2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/nf2.mma index 69b9db036..81de1d480 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/nf2.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/nf2.mma @@ -20,5 +20,5 @@ include "Basic-2/nf2/dec.ma". include "Basic-2/nf2/pr3.ma". -inline procedural "Basic-1/sn3/nf2.ma". +inline "Basic-1/sn3/nf2.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/props.mma index 9e37a001f..3244a5237 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/props.mma @@ -22,5 +22,5 @@ include "Basic-2/nf2/iso.ma". include "Basic-2/pr3/iso.ma". -inline procedural "Basic-1/sn3/props.ma". +inline "Basic-1/sn3/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/fwd.mma index 164d6ec87..a2600b078 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/sty0/defs.ma". -inline procedural "Basic-1/sty0/fwd.ma". +inline "Basic-1/sty0/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/props.mma index 8cc6b475a..403332ea0 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/props.mma @@ -18,5 +18,5 @@ include "Basic-2/sty0/defs.ma". include "Basic-2/getl/drop.ma". -inline procedural "Basic-1/sty0/props.ma". +inline "Basic-1/sty0/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/cnt.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/cnt.mma index 2ed64e8da..062ba4446 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/cnt.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/cnt.mma @@ -18,5 +18,5 @@ include "Basic-2/sty1/props.ma". include "Basic-2/cnt/props.ma". -inline procedural "Basic-1/sty1/cnt.ma". +inline "Basic-1/sty1/cnt.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/props.mma index bf2b520fa..f764f229a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/props.mma @@ -18,5 +18,5 @@ include "Basic-2/sty1/defs.ma". include "Basic-2/sty0/props.ma". -inline procedural "Basic-1/sty1/props.ma". +inline "Basic-1/sty1/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/fwd.mma index 37db04461..27b37067f 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/subst/defs.ma". -inline procedural "Basic-1/subst/fwd.ma". +inline "Basic-1/subst/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/props.mma index 594ca5f8d..1a45f22b5 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst/props.mma @@ -20,5 +20,5 @@ include "Basic-2/subst0/defs.ma". include "Basic-2/lift/props.ma". -inline procedural "Basic-1/subst/props.ma". +inline "Basic-1/subst/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/dec.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/dec.mma index 6c7b88798..b6595349c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/dec.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/dec.mma @@ -18,5 +18,5 @@ include "Basic-2/subst0/defs.ma". include "Basic-2/lift/props.ma". -inline procedural "Basic-1/subst0/dec.ma". +inline "Basic-1/subst0/dec.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/fwd.mma index 9e17f7c73..3da14bb5e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/fwd.mma @@ -18,5 +18,5 @@ include "Basic-2/subst0/defs.ma". include "Basic-2/lift/props.ma". -inline procedural "Basic-1/subst0/fwd.ma". +inline "Basic-1/subst0/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/props.mma index 88bbcf44b..155ba9e4f 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/props.mma @@ -16,5 +16,5 @@ include "Basic-2/subst0/fwd.ma". -inline procedural "Basic-1/subst0/props.ma". +inline "Basic-1/subst0/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/subst0.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/subst0.mma index fa45dec28..3e87d4560 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/subst0.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/subst0.mma @@ -16,5 +16,5 @@ include "Basic-2/subst0/props.ma". -inline procedural "Basic-1/subst0/subst0.ma". +inline "Basic-1/subst0/subst0.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/tlt.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/tlt.mma index fa103084e..6583c3c92 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/tlt.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/tlt.mma @@ -20,5 +20,5 @@ include "Basic-2/lift/props.ma". include "Basic-2/lift/tlt.ma". -inline procedural "Basic-1/subst0/tlt.ma". +inline "Basic-1/subst0/tlt.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/fwd.mma index 14fce8c8f..78669f892 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/fwd.mma @@ -18,5 +18,5 @@ include "Basic-2/subst1/defs.ma". include "Basic-2/subst0/props.ma". -inline procedural "Basic-1/subst1/fwd.ma". +inline "Basic-1/subst1/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/props.mma index 3ff04ea10..35ae5d43d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/props.mma @@ -18,5 +18,5 @@ include "Basic-2/subst1/defs.ma". include "Basic-2/subst0/props.ma". -inline procedural "Basic-1/subst1/props.ma". +inline "Basic-1/subst1/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/subst1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/subst1.mma index 83161a5f2..af3f35761 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/subst1.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/subst1.mma @@ -18,5 +18,5 @@ include "Basic-2/subst1/fwd.ma". include "Basic-2/subst0/subst0.ma". -inline procedural "Basic-1/subst1/subst1.ma". +inline "Basic-1/subst1/subst1.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/tlist/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/tlist/props.mma index 565faf6f7..4fcfcb1fb 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/tlist/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/tlist/props.mma @@ -16,5 +16,5 @@ include "Basic-2/tlist/defs.ma". -inline procedural "Basic-1/tlist/props.ma". +inline "Basic-1/tlist/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/tlt/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/tlt/props.mma index 70a1a12f1..75aff34af 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/tlt/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/tlt/props.mma @@ -16,5 +16,5 @@ include "Basic-2/tlt/defs.ma". -inline procedural "Basic-1/tlt/props.ma". +inline "Basic-1/tlt/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity.mma index 73842ed6d..a50d25340 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity.mma @@ -20,5 +20,5 @@ include "Basic-2/arity/pr3.ma". include "Basic-2/asucc/fwd.ma". -inline procedural "Basic-1/ty3/arity.ma". +inline "Basic-1/ty3/arity.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity_props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity_props.mma index 0d8990552..65475e81c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity_props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity_props.mma @@ -18,5 +18,5 @@ include "Basic-2/ty3/arity.ma". include "Basic-2/sc3/arity.ma". -inline procedural "Basic-1/ty3/arity_props.ma". +inline "Basic-1/ty3/arity_props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/dec.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/dec.mma index f6d6c6011..da5291990 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/dec.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/dec.mma @@ -20,5 +20,5 @@ include "Basic-2/getl/flt.ma". include "Basic-2/getl/dec.ma". -inline procedural "Basic-1/ty3/dec.ma". +inline "Basic-1/ty3/dec.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fsubst0.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fsubst0.mma index 6055c0c1a..11b8873da 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fsubst0.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fsubst0.mma @@ -20,5 +20,5 @@ include "Basic-2/pc3/fsubst0.ma". include "Basic-2/getl/getl.ma". -inline procedural "Basic-1/ty3/fsubst0.ma". +inline "Basic-1/ty3/fsubst0.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd.mma index b23abe7dd..c019d001a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd.mma @@ -18,5 +18,5 @@ include "Basic-2/ty3/defs.ma". include "Basic-2/pc3/props.ma". -inline procedural "Basic-1/ty3/fwd.ma". +inline "Basic-1/ty3/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd_nf2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd_nf2.mma index e5e5c669f..6894ae466 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd_nf2.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd_nf2.mma @@ -20,5 +20,5 @@ include "Basic-2/pc3/nf2.ma". include "Basic-2/nf2/fwd.ma". -inline procedural "Basic-1/ty3/fwd_nf2.ma". +inline "Basic-1/ty3/fwd_nf2.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/nf2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/nf2.mma index b6ccdfe06..af7960855 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/nf2.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/nf2.mma @@ -20,5 +20,5 @@ include "Basic-2/pc3/nf2.ma". include "Basic-2/nf2/arity.ma". -inline procedural "Basic-1/ty3/nf2.ma". +inline "Basic-1/ty3/nf2.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3.mma index 143c7f140..dd43847bd 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3.mma @@ -26,5 +26,5 @@ include "Basic-2/pc3/wcpr0.ma". include "Basic-2/pc1/props.ma". -inline procedural "Basic-1/ty3/pr3.ma". +inline "Basic-1/ty3/pr3.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3_props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3_props.mma index df88edd87..a352ace49 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3_props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3_props.mma @@ -16,5 +16,5 @@ include "Basic-2/ty3/pr3.ma". -inline procedural "Basic-1/ty3/pr3_props.ma". +inline "Basic-1/ty3/pr3_props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/props.mma index 3dc7568c2..c5e6cb33e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/props.mma @@ -18,5 +18,5 @@ include "Basic-2/ty3/fwd.ma". include "Basic-2/pc3/fwd.ma". -inline procedural "Basic-1/ty3/props.ma". +inline "Basic-1/ty3/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/sty0.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/sty0.mma index ad7ff0cfa..0c5ebc151 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/sty0.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/sty0.mma @@ -18,5 +18,5 @@ include "Basic-2/ty3/pr3_props.ma". include "Basic-2/sty0/fwd.ma". -inline procedural "Basic-1/ty3/sty0.ma". +inline "Basic-1/ty3/sty0.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/subst1.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/subst1.mma index acdee271b..97f45a1ec 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/subst1.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/subst1.mma @@ -20,5 +20,5 @@ include "Basic-2/pc3/subst1.ma". include "Basic-2/getl/getl.ma". -inline procedural "Basic-1/ty3/subst1.ma". +inline "Basic-1/ty3/subst1.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/fwd.mma index 1dc828d8e..0a9a87638 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/wcpr0/defs.ma". -inline procedural "Basic-1/wcpr0/fwd.ma". +inline "Basic-1/wcpr0/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/getl.mma index 01c20904e..e412692e5 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/getl.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/getl.mma @@ -18,5 +18,5 @@ include "Basic-2/wcpr0/defs.ma". include "Basic-2/getl/props.ma". -inline procedural "Basic-1/wcpr0/getl.ma". +inline "Basic-1/wcpr0/getl.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/clear.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/clear.mma index d37a5f89d..e63bb3e82 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/clear.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/clear.mma @@ -16,5 +16,5 @@ include "Basic-2/wf3/fwd.ma". -inline procedural "Basic-1/wf3/clear.ma". +inline "Basic-1/wf3/clear.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/fwd.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/fwd.mma index 368615dab..73bf245a7 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/fwd.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/fwd.mma @@ -16,5 +16,5 @@ include "Basic-2/wf3/defs.ma". -inline procedural "Basic-1/wf3/fwd.ma". +inline "Basic-1/wf3/fwd.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/getl.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/getl.mma index 1437739af..fe6e74042 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/getl.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/getl.mma @@ -18,5 +18,5 @@ include "Basic-2/wf3/clear.ma". include "Basic-2/ty3/dec.ma". -inline procedural "Basic-1/wf3/getl.ma". +inline "Basic-1/wf3/getl.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/props.mma index a26ff78ca..35a6a6474 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/props.mma @@ -18,5 +18,5 @@ include "Basic-2/wf3/ty3.ma". include "Basic-2/app/defs.ma". -inline procedural "Basic-1/wf3/props.ma". +inline "Basic-1/wf3/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/ty3.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/ty3.mma index cf3cbd160..8af324db5 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/ty3.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/ty3.mma @@ -16,5 +16,5 @@ include "Basic-2/wf3/getl.ma". -inline procedural "Basic-1/wf3/ty3.ma". +inline "Basic-1/wf3/ty3.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/blt/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/blt/props.mma index fb23f3047..24fd85f96 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/blt/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/blt/props.mma @@ -16,5 +16,5 @@ include "Ground-2/blt/defs.ma". -inline procedural "Ground-1/blt/props.ma". +inline "Ground-1/blt/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/ext/arith.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/ext/arith.mma index 8cce7155b..ab8a4c76e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/ext/arith.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/ext/arith.mma @@ -16,5 +16,5 @@ include "Ground-2/preamble.ma". -inline procedural "Ground-1/ext/arith.ma". +inline "Ground-1/ext/arith.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/ext/tactics.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/ext/tactics.mma index 80924a6d3..72cacebfc 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/ext/tactics.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/ext/tactics.mma @@ -16,5 +16,5 @@ include "Ground-2/preamble.ma". -inline procedural "Ground-1/ext/tactics.ma". +inline "Ground-1/ext/tactics.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/plist/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/plist/props.mma index 97eea3400..196cf33a7 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/plist/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/plist/props.mma @@ -16,5 +16,5 @@ include "Ground-2/plist/defs.ma". -inline procedural "Ground-1/plist/props.ma". +inline "Ground-1/plist/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/types/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/types/props.mma index e06bb4d91..49444e73b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/types/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-2/types/props.mma @@ -16,5 +16,5 @@ include "Ground-2/types/defs.ma". -inline procedural "Ground-1/types/props.ma". +inline "Ground-1/types/props.ma" procedural. diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/props.mma index bd916f9cb..e214da177 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/props.mma @@ -16,5 +16,5 @@ include "Legacy-2/coq/defs.ma". -inline procedural "Legacy-1/coq/props.ma". +inline "Legacy-1/coq/props.ma" procedural. -- 2.39.2