From: Ferruccio Guidi Date: Tue, 11 Oct 2011 17:43:01 +0000 (+0000) Subject: update ... X-Git-Tag: make_still_working~2207 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9b077c63115106e3b61a4f06f5c03f7a059e7f45;p=helm.git update ... --- diff --git a/helm/www/lambda_delta/bin/xhtbl/Makefile.common b/helm/www/lambda_delta/bin/xhtbl/Makefile.common index 96c564336..63df6873d 100644 --- a/helm/www/lambda_delta/bin/xhtbl/Makefile.common +++ b/helm/www/lambda_delta/bin/xhtbl/Makefile.common @@ -1,6 +1,6 @@ H=@ -include ../../../claudio/Makefile.defs +include Makefile.defs DIST=$(EXEC)---$(VERSION) DATE=$(shell date +%y%m%d) diff --git a/helm/www/lambda_delta/bin/xhtbl/Makefile.defs b/helm/www/lambda_delta/bin/xhtbl/Makefile.defs new file mode 100644 index 000000000..4fb7bad2d --- /dev/null +++ b/helm/www/lambda_delta/bin/xhtbl/Makefile.defs @@ -0,0 +1,19 @@ +ifeq ($(origin OCAMLPATH), undefined) +OCAMLFIND = OCAMLPATH=/home/fguidi/svn/helm-stable/software/components/METAS ocamlfind +else +OCAMLFIND = ocamlfind +endif +CAMLP5O = camlp5o +LABLGLADECC = lablgladecc2 +HAVE_OCAMLOPT = yes +DISTRIBUTED = no +ANNOT = false + +MATITA_REQUIRES = helm-disambiguation helm-cic_disambiguation helm-grafite helm-grafite_engine helm-tptp_grafite helm-ng_disambiguation helm-ng_cic_content helm-grafite_parser helm-acic_procedural helm-content_pres helm-hgdome helm-tactics helm-ng_paramodulation helm-ng_tactics helm-cic_exportation lablgtk2.glade lablgtkmathview lablgtksourceview2.gtksourceview2 helm-xmldiff +MATITA_CREQUIRES = helm-disambiguation helm-cic_disambiguation helm-grafite helm-grafite_engine helm-tptp_grafite helm-ng_disambiguation helm-ng_cic_content helm-grafite_parser helm-acic_procedural helm-content_pres helm-hgdome helm-tactics helm-ng_paramodulation helm-ng_tactics helm-cic_exportation + +MATITA_VERSION = 0.5.8 + +SRCROOT = /home/fguidi/svn/helm-stable/software +RT_BASE_DIR = /home/fguidi/svn/helm-stable/software/matita +DBHOST = mysql://mowgli.cs.unibo.it diff --git a/helm/www/lambda_delta/ld_basic_2.html b/helm/www/lambda_delta/ld_basic_2.html index 1110c7060..58087e46d 100644 --- a/helm/www/lambda_delta/ld_basic_2.html +++ b/helm/www/lambda_delta/ld_basic_2.html @@ -16,7 +16,7 @@

cic:/matita/lambda_delta/Basic_2/ (Î»Î´ version 2)

Logical structure of the contribution

The source files are grouped in planes and components according to the following table.

component	plane	files
native typing		nty
conversion	context-sensitive	cpcs
computation	strongly normalizing	csn
	context-sensitive	cprs
reduction	context-sensitive	lcpr
		cpr	cpr_lift	cpr_tpss	cpr_cpr
	context-free	ltpr	ltpr_drop
		tpr	tpr_lift	tpr_tpss	tpr_tpr
static typing	atomic arity ass.	aaa	aaa_lift	aaa_aaa
	static type ass.	sty	sty_lift	sty_sty
unfold	partial	ltpss	ltpss_drop	ltpss_tps	ltpss_ltpss
		tpss	tpss_lift	tpss_tpss	tpss_ltps
substitution	parallel	ltps	ltps_drop	ltps_tps	ltps_ltps
		tps	tps_lift	tps_tps
	local env. dropping	drop	drop_drop
	term relocation	lift	lift_lift
grammar	local env. equivalence	leq	leq_leq
	term hom.	thom	thom_thom
	closures	cl_shift	cl_weight
	internal syntax	lenv	lenv_weight	lenv_length
		term	term_weight	term_simple
		item
	external syntax	aarity
	parameters	sh

component	plane	files
native typing		nty
conversion	context-sensitive	cpcs
computation	strongly normalizing	csn
	context-sensitive	cprs
reduction	context-sensitive	lcpr
		cpr	cpr_lift	cpr_tpss	cpr_cpr
	context-free	ltpr	ltpr_drop
		tpr	tpr_lift	tpr_tpss	tpr_tpr
static typing	atomic arity ass.	aaa	aaa_lift	aaa_aaa
	static type ass.	sty	sty_lift	sty_sty
unfold	partial	ltpss	ltpss_drop	ltpss_tps	ltpss_ltpss
		tpss	tpss_lift	tpss_tpss	tpss_ltps
substitution	parallel	ltps	ltps_drop	ltps_tps	ltps_ltps
		tps	tps_lift	tps_tps
	local env. dropping	drop	drop_drop
	term relocation	lift	lift_lift
grammar	local env. ref. for substitution	lsubs	lsubs_lsubs
	term hom.	thom	thom_thom
	closures	cl_shift	cl_weight
	internal syntax	lenv	lenv_weight	lenv_length
		term	term_weight	term_simple
		item
	external syntax	aarity
	parameters	sh

Physical structure of the contribution

The source files are grouped in directories, one for each component.