From: Ferruccio Guidi Date: Tue, 8 Jan 2019 15:34:20 +0000 (+0100) Subject: patches for compilation with ocaml 4.0.5 X-Git-Tag: make_still_working~229^2~2 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d8f6494f48aa08bb32d9d1ac82fc16e9e41b76ac;p=helm.git patches for compilation with ocaml 4.0.5 + lambdadelta website update --- diff --git a/helm/www/lambdadelta/images/bronze-03BB.png b/helm/www/lambdadelta/images/bronze-03BB.png new file mode 100644 index 000000000..3cf590000 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 8e6135836..e773b460b 100644 --- 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 Unicode support. + + + diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl index 3fbc83b45..82ce7d781 100644 --- a/helm/www/lambdadelta/xslt/ld_web_root.xsl +++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl @@ -190,6 +190,14 @@ + + [Official bronze sponsor of Unicode Consortium] + +

diff --git a/matita/components/Makefile.common b/matita/components/Makefile.common index 922a0e132..74a54a821 100644 --- 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 665df181e..16f079f48 100644 --- 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