From 78b677a78cbe8f6f71ebdcdff970d0cde8a8c1b8 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 18 Mar 2008 19:22:41 +0000 Subject: [PATCH] LAMBDA-TYPES: level 2 dependences are now correct, at least :) --- .../contribs/LAMBDA-TYPES/Legacy-2/.depend | 2 + .../LAMBDA-TYPES/Legacy-2/coq/defs.mma | 20 ++++++++++ .../LAMBDA-TYPES/Legacy-2/coq/props.mma | 20 ++++++++++ .../contribs/LAMBDA-TYPES/Legacy-2/depends | 2 + .../LAMBDA-TYPES/Legacy-2/preamble.ma | 40 +++++++++++++++++++ .../contribs/LAMBDA-TYPES/Legacy-2/theory.ma | 18 +++++++++ .../matita/contribs/LAMBDA-TYPES/Makefile | 16 +++++--- 7 files changed, 112 insertions(+), 6 deletions(-) create mode 100644 helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/.depend create mode 100644 helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/defs.mma create mode 100644 helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/props.mma create mode 100644 helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/depends create mode 100644 helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma create mode 100644 helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/theory.ma diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/.depend b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/.depend new file mode 100644 index 000000000..925c30793 --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/.depend @@ -0,0 +1,2 @@ +Legacy-2/coq/defs.ma: Legacy-2/coq/defs.mma Legacy-2/preamble.ma +Legacy-2/coq/props.ma: Legacy-2/coq/props.mma Legacy-2/coq/defs.ma diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/defs.mma b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/defs.mma new file mode 100644 index 000000000..a2dd820a1 --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/defs.mma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +include "Legacy-2/preamble.ma". + +inline procedural "Legacy-1/coq/defs.ma". + 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 new file mode 100644 index 000000000..bd916f9cb --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/props.mma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +include "Legacy-2/coq/defs.ma". + +inline procedural "Legacy-1/coq/props.ma". + diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/depends b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/depends new file mode 100644 index 000000000..0faac1049 --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/depends @@ -0,0 +1,2 @@ +Legacy-2/coq/defs.mma Legacy-2/preamble.ma Legacy-1/coq/defs.ma +Legacy-2/coq/props.mma Legacy-2/preamble.ma Legacy-1/coq/props.ma diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma new file mode 100644 index 000000000..269e41d6a --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma @@ -0,0 +1,40 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Legacy-1/definitions.ma". +(* +default "equality" + cic:/Coq/Init/Logic/eq.ind + cic:/Coq/Init/Logic/sym_eq.con + cic:/Coq/Init/Logic/trans_eq.con + cic:/Coq/Init/Logic/eq_ind.con + cic:/Coq/Init/Logic/eq_ind_r.con + cic:/Coq/Init/Logic/eq_rec.con + cic:/Coq/Init/Logic/eq_rec_r.con + cic:/Coq/Init/Logic/eq_rect.con + cic:/Coq/Init/Logic/eq_rect_r.con + cic:/Coq/Init/Logic/f_equal.con + cic:/matita/legacy/coq/f_equal1.con. + +default "true" + cic:/Coq/Init/Logic/True.ind. +default "false" + cic:/Coq/Init/Logic/False.ind. +default "absurd" + cic:/Coq/Init/Logic/absurd.con. + +(* aritmetic operators *) + +interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y). +*) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/theory.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/theory.ma new file mode 100644 index 000000000..5cd562260 --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/theory.ma @@ -0,0 +1,18 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +include "Legacy-2/coq/props.ma". + diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile index 0ccf2514a..32da5d327 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile @@ -4,9 +4,9 @@ MATITAOPTIONS=$(MATITAUSEROPTIONS) -onepass DIR=$(shell basename $$PWD) -MMAS = $(shell find -name "*.mma") # Base-2 +MMAS = $(shell find Legacy-2 Base-2 -name "*.mma") MAS = $(MMAS:%.mma=%.ma) -XMAS = Base-2/theory.ma LambdaDelta-2/theory.ma +XMAS = Legacy-2/theory.ma Base-2/theory.ma LambdaDelta-2/theory.ma $(DIR) all: depends $(H)$(MAKE) H=$(H) --no-print-directory build @@ -15,11 +15,13 @@ $(DIR).opt opt all.opt: depends $(H)$(MAKE) H=$(H) --no-print-directory build.opt build: $(MAS) - $(H)$echo Base-2/theory.ma `../../matitadep.opt -stdout Base-2/theory.ma` >> depends + $(H)echo Legacy-2/theory.ma `../../matitadep.opt -stdout Legacy-2/theory.ma` >> depends + $(H)echo Base-2/theory.ma `../../matitadep.opt -stdout Base-2/theory.ma` >> depends $(H)../../matitac $(MATITAOPTIONS) 2> /dev/null $(H)rm depends build.opt: $(MAS) + $(H)echo Legacy-2/theory.ma `../../matitadep.opt -stdout Legacy-2/theory.ma` >> depends $(H)echo Base-2/theory.ma `../../matitadep.opt -stdout Base-2/theory.ma` >> depends $(H)../../matitac.opt $(MATITAOPTIONS) 2> /dev/null $(H)rm depends @@ -39,11 +41,12 @@ clean.ma: depend: @echo matitadep $(H)../../matitadep $(foreach FILE,$(XMAS),-exclude $(FILE)) -# $(H)cat Base-2/depends >> depends + $(H)cat Legacy-2/depends Base-2/depends >> depends + depend.opt: @echo matitadep.opt $(H)../../matitadep.opt $(foreach FILE,$(XMAS),-exclude $(FILE)) -# $(H)cat Base-2/depends >> depends + $(H)cat Legacy-2/depends Base-2/depends >> depends depends: depend.opt @@ -52,4 +55,5 @@ depends: depend.opt $(H)../../matitac.opt $(MATITAOPTIONS) -dump $@ $< 2> /dev/null $(H)echo $@ `../../matitadep.opt -stdout $@` >> depends -#include Base-2/.depend +include Legacy-2/.depend +include Base-2/.depend -- 2.39.2