From 474586cb3917d3961bbf1e8b818b83073dc510f2 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 12 Feb 2008 16:21:19 +0000 Subject: [PATCH] renaming --- .../contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma | 3 +++ .../contribs/LAMBDA-TYPES/Base-2/blt/props2.mma | 4 +++- .../contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma | 4 ++++ .../contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma | 2 ++ .../contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma | 2 ++ .../contribs/LAMBDA-TYPES/Base-2/plist/props2.mma | 4 +++- .../matita/contribs/LAMBDA-TYPES/Base-2/root | 1 - .../matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma | 12 +++++++----- .../contribs/LAMBDA-TYPES/Base-2/types/defs2.mma | 5 +++++ .../contribs/LAMBDA-TYPES/Base-2/types/props2.mma | 4 +++- 10 files changed, 32 insertions(+), 9 deletions(-) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma index 6eb948342..12438b398 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma @@ -14,7 +14,10 @@ (* This file was automatically generated: do not edit *********************) +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt/defs". + include "preamble.ma". + (* object blt not inlined *) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma index 1fd2047fd..d24466394 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma @@ -14,7 +14,9 @@ (* This file was automatically generated: do not edit *********************) -include "blt/defs2.ma". +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt/props". + +include "blt/defs.ma". inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/lt_blt.con". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma index 436b497c9..0047b1438 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma @@ -14,6 +14,8 @@ (* This file was automatically generated: do not edit *********************) +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext/arith". + include "preamble.ma". inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/nat_dec.con". @@ -21,6 +23,8 @@ inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/nat_dec.con". inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/simpl_plus_r.con". +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_Sx_Sy.con". + inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_plus_r.con". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma index e6b75198a..18de7f71a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma @@ -14,6 +14,8 @@ (* This file was automatically generated: do not edit *********************) +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics". + include "preamble.ma". inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/insert_eq.con". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma index 4ae6d5156..3dc03da0b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma @@ -14,6 +14,8 @@ (* This file was automatically generated: do not edit *********************) +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/defs". + include "preamble.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma index f9cec902e..29357a88a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma @@ -14,7 +14,9 @@ (* This file was automatically generated: do not edit *********************) -include "plist/defs2.ma". +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/props". + +include "plist/defs.ma". inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/plist/props/papp_ss.con". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/root b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/root index 229adbd73..ef1f7b21e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/root +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/root @@ -1,2 +1 @@ baseuri=cic:/matita/LAMBDA-TYPES/Base-2 -include_paths= ../Base-1 ../../../legacy diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma index d1a0ca8b4..1adab3e2b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma @@ -14,13 +14,15 @@ (* This file was automatically generated: do not edit *********************) -include "ext/tactics2.ma". +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/theory". -include "ext/arith2.ma". +include "ext/tactics.ma". -include "types/props2.ma". +include "ext/arith.ma". -include "blt/props2.ma". +include "types/props.ma". -include "plist/props2.ma". +include "blt/props.ma". + +include "plist/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma index 594edd269..87c3378c2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma @@ -14,6 +14,8 @@ (* This file was automatically generated: do not edit *********************) +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/defs". + include "preamble.ma". @@ -23,6 +25,9 @@ include "preamble.ma". (* object and4 not inlined *) +(* object and5 not inlined *) + + (* object or3 not inlined *) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma index 10b502461..d79bfc46b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma @@ -14,7 +14,9 @@ (* This file was automatically generated: do not edit *********************) -include "types/defs2.ma". +set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/props". + +include "types/defs.ma". inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/types/props/ex2_sym.con". -- 2.39.2