From: Ferruccio Guidi Date: Sat, 1 Jun 2013 16:42:29 +0000 (+0000) Subject: update in basic_2 and apps_2 X-Git-Tag: make_still_working~1141 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=54a4872ce3e05e56ca36747df014aa506bd9c71d update in basic_2 and apps_2 --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index 40a8fa2f3..17efe350b 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Thu, 16 May 2013 16:37:26 +0200
+
Last update: Sat, 01 Jun 2013 18:41:06 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index f8b26841b..6e81b110f 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -72,29 +72,29 @@ sizes files - 5 + 4 characters - 5790 + 3928 nodes - 9846 + 3637 propositions theorems - 4 + 2 lemmas 1 total - 5 + 3 concepts declared 3 defined - 10 + 9 total - 13 + 12 @@ -138,29 +138,17 @@ - MLTT1 - - genv_primitive - judgement + functional + reduction and type machine + rtm + rtm_step ( ? ⇨ ? ) - functional - reduction and type machine - rtm - rtm_step ( ? ⇨ ? ) - - - +
- unfold - lift ( ↑[?,?] ? ) - subst ( [?←?] ? ) - - - examples - - + relocation + lift ( ↑[?,?] ? )
@@ -199,6 +187,6 @@

-
Last update: Thu, 16 May 2013 16:37:26 +0200
+
Last update: Sat, 01 Jun 2013 18:41:06 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index 3766523d5..9d7141b4c 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -161,18 +161,18 @@ files 169 characters - 347556 + 348328 nodes - 969490 + 970177 propositions theorems 75 lemmas - 707 + 716 total - 782 + 791 concepts @@ -1004,6 +1004,6 @@

-
Last update: Thu, 16 May 2013 16:37:26 +0200
+
Last update: Sat, 01 Jun 2013 18:41:06 +0200
diff --git a/helm/www/lambdadelta/bin/Makefile.common b/helm/www/lambdadelta/bin/Makefile.common new file mode 100644 index 000000000..bf944971b --- /dev/null +++ b/helm/www/lambdadelta/bin/Makefile.common @@ -0,0 +1,27 @@ +H=@ + +include ../../etc/Makefile.defs + +DIST=$(EXEC)---$(VERSION) +DATE=$(shell date +%y%m%d) + +OCAMLOPTIONS = -linkpkg -thread -rectypes -package \"$(REQUIRES)\" +OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) +OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) + +all: $(EXEC).native + +$(EXEC).native: $(wildcard *.ml) $(wildcard *.mli) $(wildcard *.mly) $(wildcard *.mll) + @echo " OCAMLBUILD $(EXEC).native" + $(H)ocamlbuild -ocamlc "$(OCAMLC)" -ocamlopt "$(OCAMLOPT)" -yaccflags "$(YACCFLAGS)" $(EXEC).native + +clean: + ocamlbuild -clean + rm -rf $(DIST) $(DIST).tgz + +dist: + mkdir -p $(DIST)/Sources + cp ReadMe $(DIST) + cp *.ml *.mli *.mll *.mly Makefile _tags $(DIST)/Sources + cd $(DIST); ln -s Sources/$(EXEC).native $(EXEC) + tar -cvzf $(DIST).tgz $(DIST) diff --git a/helm/www/lambdadelta/bin/xhtbl/Makefile b/helm/www/lambdadelta/bin/xhtbl/Makefile index c9bea1a53..e1b330db9 100644 --- a/helm/www/lambdadelta/bin/xhtbl/Makefile +++ b/helm/www/lambdadelta/bin/xhtbl/Makefile @@ -5,7 +5,7 @@ REQUIRES = str YACCFLAGS = -v -include Makefile.common +include ../Makefile.common test: @$(MAKE) --no-print-directory -C ../../ www diff --git a/helm/www/lambdadelta/bin/xhtbl/Makefile.common b/helm/www/lambdadelta/bin/xhtbl/Makefile.common deleted file mode 100644 index bf944971b..000000000 --- a/helm/www/lambdadelta/bin/xhtbl/Makefile.common +++ /dev/null @@ -1,27 +0,0 @@ -H=@ - -include ../../etc/Makefile.defs - -DIST=$(EXEC)---$(VERSION) -DATE=$(shell date +%y%m%d) - -OCAMLOPTIONS = -linkpkg -thread -rectypes -package \"$(REQUIRES)\" -OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) -OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) - -all: $(EXEC).native - -$(EXEC).native: $(wildcard *.ml) $(wildcard *.mli) $(wildcard *.mly) $(wildcard *.mll) - @echo " OCAMLBUILD $(EXEC).native" - $(H)ocamlbuild -ocamlc "$(OCAMLC)" -ocamlopt "$(OCAMLOPT)" -yaccflags "$(YACCFLAGS)" $(EXEC).native - -clean: - ocamlbuild -clean - rm -rf $(DIST) $(DIST).tgz - -dist: - mkdir -p $(DIST)/Sources - cp ReadMe $(DIST) - cp *.ml *.mli *.mll *.mly Makefile _tags $(DIST)/Sources - cd $(DIST); ln -s Sources/$(EXEC).native $(EXEC) - tar -cvzf $(DIST).tgz $(DIST)