From 0e9753cbccef485911e2c2de1b4cdcae592906b9 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 19 Feb 2008 17:16:12 +0000 Subject: [PATCH] we are moving the devel root one dir level up --- .../contribs/LAMBDA-TYPES/Base-1/Makefile | 15 --- .../contribs/LAMBDA-TYPES/Base-1/blt/defs.ma | 2 +- .../contribs/LAMBDA-TYPES/Base-1/blt/props.ma | 2 +- .../LAMBDA-TYPES/Base-1/definitions.ma | 6 +- .../contribs/LAMBDA-TYPES/Base-1/ext/arith.ma | 2 +- .../LAMBDA-TYPES/Base-1/ext/tactics.ma | 2 +- .../LAMBDA-TYPES/Base-1/plist/defs.ma | 2 +- .../LAMBDA-TYPES/Base-1/plist/props.ma | 2 +- .../contribs/LAMBDA-TYPES/Base-1/spare.ma | 2 +- .../contribs/LAMBDA-TYPES/Base-1/theory.ma | 10 +- .../LAMBDA-TYPES/Base-1/types/defs.ma | 10 +- .../LAMBDA-TYPES/Base-1/types/props.ma | 2 +- .../contribs/LAMBDA-TYPES/Base-2/blt/defs.mma | 5 +- .../LAMBDA-TYPES/Base-2/blt/props.mma | 10 +- .../LAMBDA-TYPES/Base-2/ext/arith.mma | 96 +------------------ .../LAMBDA-TYPES/Base-2/ext/tactics.mma | 9 +- .../LAMBDA-TYPES/Base-2/plist/defs.mma | 14 +-- .../LAMBDA-TYPES/Base-2/plist/props.mma | 4 +- .../contribs/LAMBDA-TYPES/Base-2/theory.mma | 10 +- .../LAMBDA-TYPES/Base-2/types/defs.mma | 65 +------------ .../LAMBDA-TYPES/Base-2/types/props.mma | 4 +- .../matita/contribs/LAMBDA-TYPES/Makefile | 25 +++-- .../LAMBDA-TYPES/{Base-1 => }/depends | 0 .../contribs/LAMBDA-TYPES/{Base-1 => }/root | 0 24 files changed, 61 insertions(+), 238 deletions(-) delete mode 100644 helm/software/matita/contribs/LAMBDA-TYPES/Base-1/Makefile rename helm/software/matita/contribs/LAMBDA-TYPES/{Base-1 => }/depends (100%) rename helm/software/matita/contribs/LAMBDA-TYPES/{Base-1 => }/root (100%) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/Makefile deleted file mode 100644 index a57a7281e..000000000 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/Makefile +++ /dev/null @@ -1,15 +0,0 @@ -DIR=$(shell basename $$PWD) -MATITAOPTIONS=-onepass - -$(DIR) all: - ../../../matitac $(MATITAOPTIONS) -$(DIR).opt opt all.opt: - ../../../matitac.opt $(MATITAOPTIONS) -clean: - ../../../matitaclean -clean.opt: - ../../../matitaclean.opt -depend: - ../../../matitadep -depend.opt: - ../../../matitadep.opt diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma index 293c184f5..660e18626 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "preamble.ma". +include "Base-1/preamble.ma". definition blt: nat \to (nat \to bool) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma index 3cff54f96..751dcee9c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "blt/defs.ma". +include "Base-1/blt/defs.ma". theorem lt_blt: \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq bool (blt y x) true))) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma index 3a087dec7..79cc45e28 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma @@ -14,9 +14,9 @@ (* This file was automatically generated: do not edit *********************) -include "types/defs.ma". +include "Base-1/types/defs.ma". -include "blt/defs.ma". +include "Base-1/blt/defs.ma". -include "plist/defs.ma". +include "Base-1/plist/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma index 70a94bfbd..0d0f2a5df 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "preamble.ma". +include "Base-1/preamble.ma". theorem nat_dec: \forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma index 7fcdc28ec..79551495d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "preamble.ma". +include "Base-1/preamble.ma". theorem insert_eq: \forall (S: Set).(\forall (x: S).(\forall (P: ((S \to Prop))).(\forall (G: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma index 9cfca05ae..5cf9337e4 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "preamble.ma". +include "Base-1/preamble.ma". inductive PList: Set \def | PNil: PList diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma index bc480cc23..cfe98b20d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "plist/defs.ma". +include "Base-1/plist/defs.ma". theorem papp_ss: \forall (is1: PList).(\forall (is2: PList).(eq PList (papp (Ss is1) (Ss diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma index c62e67982..024efedf4 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma @@ -14,5 +14,5 @@ (* This file was automatically generated: do not edit *********************) -include "theory.ma". +include "Base-1/theory.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/theory.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/theory.ma index c7c94ce53..3f643ffa1 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/theory.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/theory.ma @@ -14,13 +14,13 @@ (* This file was automatically generated: do not edit *********************) -include "ext/tactics.ma". +include "Base-1/ext/tactics.ma". -include "ext/arith.ma". +include "Base-1/ext/arith.ma". -include "types/props.ma". +include "Base-1/types/props.ma". -include "blt/props.ma". +include "Base-1/blt/props.ma". -include "plist/props.ma". +include "Base-1/plist/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma index cb8300ade..cddd83fd9 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "preamble.ma". +include "Base-1/preamble.ma". inductive and3 (P0: Prop) (P1: Prop) (P2: Prop): Prop \def | and3_intro: P0 \to (P1 \to (P2 \to (and3 P0 P1 P2))). @@ -92,6 +92,14 @@ Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))): Prop \def x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to (ex4_3 A0 A1 A2 P0 P1 P2 P3))))))). +inductive ex5_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to +Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to +Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))) (P4: A0 \to (A1 \to (A2 \to +Prop))): Prop \def +| ex5_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 +x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to ((P4 x0 +x1 x2) \to (ex5_3 A0 A1 A2 P0 P1 P2 P3 P4)))))))). + inductive ex3_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2: A0 \to (A1 \to (A2 \to (A3 \to Prop)))): Prop \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma index b27665600..d6f71f4a5 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "types/defs.ma". +include "Base-1/types/defs.ma". theorem ex2_sym: \forall (A: Set).(\forall (P: ((A \to Prop))).(\forall (Q: ((A \to diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma index 98bb97a68..1744bc276 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma @@ -14,8 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "preamble.ma". +include "Base-2/preamble.ma". - -(* object blt not inlined *) +inline procedural "Base-1/blt/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma index 5dfa152ee..63b209e18 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma @@ -14,13 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "blt/defs.ma". +include "Base-2/blt/defs.ma". -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/lt_blt.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/le_bge.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/blt_lt.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/bge_le.con". +inline procedural "Base-1/blt/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma index 4e73adbf7..c2e685e64 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma @@ -14,99 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "preamble.ma". +include "Base-2/preamble.ma". -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". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_permute_2_in_3.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_permute_2_in_3_assoc.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_O.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_Sx_SO.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/eq_nat_dec.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/neq_eq_e.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_false.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_Sx_x.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_n_pred.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_le.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_plus_minus_sym.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus_minus.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus_plus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_trans_plus_r.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_O.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_gen_S.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_plus_x_Sy.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/simpl_lt_plus_r.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_x_Sy.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_plus_minus.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_plus_minus_r.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_x_SO.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_x_pred_y.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_le_minus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_le_e.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_eq_e.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_eq_gt_e.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_gen_xS.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_lt_false.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_neq.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/arith0.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/O_minus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_minus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_plus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_S_minus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_pred_y.con". +inline procedural "Base-1/ext/arith.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma index e6b75198a..474b8722a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma @@ -14,12 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "preamble.ma". +include "Base-2/preamble.ma". -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/insert_eq.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/unintro.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/xinduction.con". +inline procedural "Base-1/ext/tactics.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma index 4ae6d5156..b73b56fae 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma @@ -14,17 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "preamble.ma". +include "Base-2/preamble.ma". - -(* object PList not inlined *) - - -(* object PConsTail not inlined *) - - -(* object Ss not inlined *) - - -(* object papp not inlined *) +inline procedural "Base-1/plist/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma index 130dee88c..9e21e540a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "plist/defs.ma". +include "Base-2/plist/defs.ma". -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/plist/props/papp_ss.con". +inline procedural "Base-1/plist/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma index c7c94ce53..ee1cbb7dd 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma @@ -14,13 +14,13 @@ (* This file was automatically generated: do not edit *********************) -include "ext/tactics.ma". +include "Base-2/ext/tactics.ma". -include "ext/arith.ma". +include "Base-2/ext/arith.ma". -include "types/props.ma". +include "Base-2/types/props.ma". -include "blt/props.ma". +include "Base-2/blt/props.ma". -include "plist/props.ma". +include "Base-2/plist/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma index e6ad43747..0e6405c8f 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma @@ -14,68 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "preamble.ma". +include "Base-2/preamble.ma". - -(* object and3 not inlined *) - - -(* object and4 not inlined *) - - -(* object and5 not inlined *) - - -(* object or3 not inlined *) - - -(* object or4 not inlined *) - - -(* object ex3 not inlined *) - - -(* object ex4 not inlined *) - - -(* object ex_2 not inlined *) - - -(* object ex2_2 not inlined *) - - -(* object ex3_2 not inlined *) - - -(* object ex4_2 not inlined *) - - -(* object ex_3 not inlined *) - - -(* object ex2_3 not inlined *) - - -(* object ex3_3 not inlined *) - - -(* object ex4_3 not inlined *) - - -(* object ex3_4 not inlined *) - - -(* object ex4_4 not inlined *) - - -(* object ex4_5 not inlined *) - - -(* object ex5_5 not inlined *) - - -(* object ex6_6 not inlined *) - - -(* object ex6_7 not inlined *) +inline procedural "Base-1/types/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma index b9abd1c42..1f9e38301 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -include "types/defs.ma". +include "Base-2/types/defs.ma". -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/types/props/ex2_sym.con". +inline procedural "Base-1/types/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile index 93fba67ce..a57a7281e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile @@ -1,10 +1,15 @@ -GOALS = all opt clean clean.opt - -DEVELS = Base-1 LambdaDelta-1 Base-2 Unified-Sub - -$(GOALS): - @$(foreach DEVEL, $(DEVELS), $(MAKE) -k -C $(DEVEL) $@;) - -.PHONY: (GOALS) - -.SUFFIXES: +DIR=$(shell basename $$PWD) +MATITAOPTIONS=-onepass + +$(DIR) all: + ../../../matitac $(MATITAOPTIONS) +$(DIR).opt opt all.opt: + ../../../matitac.opt $(MATITAOPTIONS) +clean: + ../../../matitaclean +clean.opt: + ../../../matitaclean.opt +depend: + ../../../matitadep +depend.opt: + ../../../matitadep.opt diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/depends b/helm/software/matita/contribs/LAMBDA-TYPES/depends similarity index 100% rename from helm/software/matita/contribs/LAMBDA-TYPES/Base-1/depends rename to helm/software/matita/contribs/LAMBDA-TYPES/depends diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/root b/helm/software/matita/contribs/LAMBDA-TYPES/root similarity index 100% rename from helm/software/matita/contribs/LAMBDA-TYPES/Base-1/root rename to helm/software/matita/contribs/LAMBDA-TYPES/root -- 2.39.2