]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: d4a98ff)
patches for compilation with ocaml 4.0.5
authorFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Tue, 8 Jan 2019 15:34:20 +0000 (16:34 +0100)
committerFerruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Tue, 8 Jan 2019 16:47:36 +0000 (17:47 +0100)
+ lambdadelta website update

helm/www/lambdadelta/images/bronze-03BB.png [new file with mode: 0644] patch | blob
helm/www/lambdadelta/web/home/home.ldw.xml patch | blob | history
helm/www/lambdadelta/xslt/ld_web_root.xsl patch | blob | history
matita/components/Makefile.common patch | blob | history
matita/matita/lib/reverse_complexity/toolkit.ma patch | blob | history

diff --git a/helm/www/lambdadelta/images/bronze-03BB.png b/helm/www/lambdadelta/images/bronze-03BB.png
new file mode 100644 (file)
index 0000000..3cf5900
Binary files /dev/null and b/helm/www/lambdadelta/images/bronze-03BB.png differ
diff --git a/helm/www/lambdadelta/web/home/home.ldw.xml b/helm/www/lambdadelta/web/home/home.ldw.xml
index 8e6135836d861a64fffbbf64e845257b950916ab..e773b460be5019d60319b3ea60b2616c14be0c21 100644 (file)
--- a/helm/www/lambdadelta/web/home/home.ldw.xml
+++ b/helm/www/lambdadelta/web/home/home.ldw.xml
@@ -30,6 +30,9 @@
       to view this site correctly, please select a font
       with <link to="http://www.unicode.org/">Unicode</link> support.
    </body>
+   <body>
+      <ucs-bronze char="03BB"/>
+   </body>
 
 <!-- ===================================================================== -->
 
diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl
index 3fbc83b4515779210127bb0179b07ad20aca34ac..82ce7d78149c5d24fd4442b892e6128bdf735911 100644 (file)
--- a/helm/www/lambdadelta/xslt/ld_web_root.xsl
+++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl
@@ -190,6 +190,14 @@
    </xsl:choose>
 </xsl:template>
 
+<xsl:template match="ld:ucs-bronze">
+   <img
+      alt="[Official bronze sponsor of Unicode Consortium]"
+      title="Official bronze sponsor of Unicode Consortium"
+      src="{$baseurl}images/bronze-{@char}.png"
+   />
+</xsl:template>
+
 <xsl:template match="ld:footer">
    <xsl:call-template name="rule"/>
    <div class="spacer"><br/></div>   
diff --git a/matita/components/Makefile.common b/matita/components/Makefile.common
index 922a0e1320ff79f24c68594ebca4209c6ad53f96..74a54a821a07a686077a04caa180e20610ab5de4 100644 (file)
--- a/matita/components/Makefile.common
+++ b/matita/components/Makefile.common
@@ -20,7 +20,7 @@ endif
 PREPROCOPTIONS = -pp camlp5o
 SYNTAXOPTIONS = -syntax camlp5o
 PREREQ =
-OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7
+OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread -rectypes $(ANNOTOPTION) -w @A-52-4-34-37-45-9-44-48-6-32-20-58-7-57-3 # -57-3 for ocaml 4.0.5
 OCAMLDEBUGOPTIONS = -g
 #OCAML_PROF=p -p a
 OCAMLARCHIVEOPTIONS =
diff --git a/matita/matita/lib/reverse_complexity/toolkit.ma b/matita/matita/lib/reverse_complexity/toolkit.ma
index 665df181e7f05321ae2ebf22bde818c0c2e7a2c0..16f079f48579ef00dc4458e9f5dea9369354397c 100644 (file)
--- a/matita/matita/lib/reverse_complexity/toolkit.ma
+++ b/matita/matita/lib/reverse_complexity/toolkit.ma
@@ -385,6 +385,19 @@ lemma max_prim_rec: ∀a,b,p,f,x. a ≤b →
   ]
 qed.
 
+(* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)
+alias symbol "pair" (instance 15) = "abstract pair".
+alias symbol "minus" (instance 14) = "natural minus".
+alias symbol "plus" (instance 11) = "natural plus".
+alias symbol "pair" (instance 10) = "abstract pair".
+alias symbol "plus" (instance 13) = "natural plus".
+alias symbol "pair" (instance 12) = "abstract pair".
+alias symbol "plus" (instance 8) = "natural plus".
+alias symbol "pair" (instance 7) = "abstract pair".
+alias symbol "plus" (instance 6) = "natural plus".
+alias symbol "pair" (instance 5) = "abstract pair".
+alias id "max" = "cic:/matita/arithmetics/nat/max#def:2".
+alias symbol "minus" (instance 3) = "natural minus".
 lemma max_prim_rec1: ∀a,b,p,f,x.
   max_{i ∈[a x,b x[ | p 〈i,x〉 }(f 〈i,x〉) = 
     prim_rec (λi.0) 
@@ -415,6 +428,19 @@ lemma sum_prim_rec1: ∀a,b,p,f,x.
   ]
 qed.
 
+(* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)
+alias symbol "pair" (instance 15) = "abstract pair".
+alias symbol "minus" (instance 14) = "natural minus".
+alias symbol "plus" (instance 11) = "natural plus".
+alias symbol "pair" (instance 10) = "abstract pair".
+alias symbol "plus" (instance 13) = "natural plus".
+alias symbol "pair" (instance 12) = "abstract pair".
+alias symbol "plus" (instance 8) = "natural plus".
+alias symbol "pair" (instance 7) = "abstract pair".
+alias symbol "pair" (instance 6) = "abstract pair".
+alias symbol "plus" (instance 4) = "natural plus".
+alias symbol "pair" (instance 3) = "abstract pair".
+alias symbol "minus" (instance 2) = "natural minus".
 lemma bigop_prim_rec: ∀a,b,c,p,f,x.
   bigop (b x-a x) (λi:ℕ.p 〈i+a x,x〉) ? (c 〈a x,x〉) plus (λi:ℕ.f 〈i+a x,x〉) = 
     prim_rec c 
@@ -430,6 +456,19 @@ lemma bigop_prim_rec: ∀a,b,c,p,f,x.
   ]
 qed.
 
+(* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)
+alias symbol "pair" (instance 15) = "abstract pair".
+alias symbol "minus" (instance 14) = "natural minus".
+alias symbol "minus" (instance 11) = "natural minus".
+alias symbol "pair" (instance 10) = "abstract pair".
+alias symbol "minus" (instance 13) = "natural minus".
+alias symbol "pair" (instance 12) = "abstract pair".
+alias symbol "minus" (instance 8) = "natural minus".
+alias symbol "pair" (instance 7) = "abstract pair".
+alias symbol "pair" (instance 6) = "abstract pair".
+alias symbol "minus" (instance 4) = "natural minus".
+alias symbol "pair" (instance 3) = "abstract pair".
+alias symbol "minus" (instance 2) = "natural minus".
 lemma bigop_prim_rec_dec: ∀a,b,c,p,f,x.
   bigop (b x-a x) (λi:ℕ.p 〈b x -i,x〉) ? (c 〈b x,x〉) plus (λi:ℕ.f 〈b x-i,x〉) = 
     prim_rec c 
@@ -492,7 +531,12 @@ qed.
 
 (* the argument is 〈b-a,〈a,x〉〉 *)
 
-
+(* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)
+alias symbol "plus" (instance 3) = "natural plus".
+alias symbol "pair" (instance 2) = "abstract pair".
+alias id "max" = "cic:/matita/arithmetics/nat/max#def:2".
+alias symbol "plus" (instance 5) = "natural plus".
+alias symbol "pair" (instance 4) = "abstract pair".
 definition max_unary_pr ≝ λp,f.unary_pr (λx.0) 
     (λi. 
       let k ≝ fst i in
@@ -529,7 +573,14 @@ definition unary_compl ≝ λp,f,hf.
           let (x:ℕ) ≝snd (snd (snd i)) in 
           if p 〈k+a,x〉 then max (f 〈k+a,x〉) r else r )) 〈fst x,snd (snd x)〉,
       snd (snd x)〉〉). *)
-      
+
+(* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)   
+alias symbol "plus" (instance 6) = "natural plus".
+alias symbol "pair" (instance 5) = "abstract pair".
+alias symbol "plus" (instance 4) = "natural plus".
+alias symbol "pair" (instance 3) = "abstract pair".
+alias symbol "plus" (instance 2) = "natural plus".
+alias symbol "plus" (instance 1) = "natural plus".
 definition aux_compl ≝ λhp,hf.λi.
   let k ≝ fst i in 
   let r ≝ fst (snd i) in 
@@ -747,7 +798,10 @@ qed.
 
 (* cambiare qui: togliere S *)
 
-
+(* FG: aliases added by matita compiled with OCaml 4.0.5, bah ??? *)
+alias symbol "minus" (instance 1) = "natural minus".
+alias symbol "minus" (instance 3) = "natural minus".
+alias symbol "pair" (instance 2) = "abstract pair".
 definition minim_unary_pr ≝ λf.unary_pr (λx.S(fst x))
     (λi. 
       let k ≝ fst i in
Unnamed repository; edit this file 'description' to name the repository.