From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 14 Jun 2021 14:28:21 +0000 (+0200)
Subject: λδ site update
X-Git-Tag: make_still_working~143
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=dfa1cda217f6b9a871ecbdd9bc54920f4a78d301

λδ site update

+ one citation added to home page
+ one bug fixed in xhtbl.ml
+ ome comment added in gcp_cr.ma
---

diff --git a/helm/www/lambdadelta/web/home/home.ldw.xml b/helm/www/lambdadelta/web/home/home.ldw.xml
index ec5cf0d07..d12eea80c 100644
--- a/helm/www/lambdadelta/web/home/home.ldw.xml
+++ b/helm/www/lambdadelta/web/home/home.ldw.xml
@@ -59,6 +59,12 @@
       This is a list of publications citing λδ documentation.
    </body>
 
+   <topitem name="C11">
+      Yaoshun Fu, Wensheng Yu:
+      <notice class="alpha">Formalizing Calculus without Limit Theory in Coq</notice>
+      (2021). In Mathematics, 9(12), pp. 1377:1-1377:24.
+   </topitem>
+
    <topitem name="C10">
       M. Weber:
       <notice class="alpha">An extended type system with lambda-typed lambda-expressions</notice>
diff --git a/matita/matita/contribs/lambdadelta/bin/xhtbl/xhtbl.ml b/matita/matita/contribs/lambdadelta/bin/xhtbl/xhtbl.ml
index 6c5f8b01f..0def8fa61 100644
--- a/matita/matita/contribs/lambdadelta/bin/xhtbl/xhtbl.ml
+++ b/matita/matita/contribs/lambdadelta/bin/xhtbl/xhtbl.ml
@@ -2,7 +2,7 @@ module A = Arg
 module F = Filename
 module L = List
 
-module O  = Options 
+module O  = Options
 module TP = TextParser
 module TL = TextLexer
 module TU = TextUnparser
@@ -48,30 +48,33 @@ let process_directive och bname (name, table, css, uri, ext) =
 
 let process_file fname =
    let bname = F.chop_extension (F.basename fname) in
-   let ich = open_in fname in
-   let lexbuf = Lexing.from_channel ich in
-   let ns, ds = TP.script TL.token lexbuf in
-   close_in ich; includes := bname :: !includes;
-   let ns = ("", "http://www.w3.org/1999/xhtml") :: ns in
-   let och = XU.open_out bname ns in 
-   L.iter (process_directive och bname) ds;
-   XU.close_out och
+   if List.mem bname !includes then ()
+   else begin
+      let ich = open_in fname in
+      let lexbuf = Lexing.from_channel ich in
+      let ns, ds = TP.script TL.token lexbuf in
+      close_in ich; includes := bname :: !includes;
+      let ns = ("", "http://www.w3.org/1999/xhtml") :: ns in
+      let och = XU.open_out bname ns in
+      L.iter (process_directive och bname) ds;
+      XU.close_out och
+   end
 
 let main () =
    A.parse [
       "-L", A.Set O.debug_lexer, help_L;
-      "-O", A.String ((:=) O.output_dir), help_O; 
+      "-O", A.String ((:=) O.output_dir), help_O;
       "-X", A.Unit O.clear, help_X;
       "-b", A.String ((:=) O.baseuri), help_b;
-      "-d0", A.Set O.d0, help_d0;  
-      "-d1", A.Set O.d1, help_d1;  
-      "-d2", A.Set O.d2, help_d2;  
-      "-e1", A.Set O.e1, help_e1;  
-      "-e2", A.Set O.e2, help_e2;  
-      "-p0", A.Set O.p0, help_p0;  
-      "-p1", A.Set O.p1, help_p1;  
-      "-p2", A.Set O.p2, help_p2;  
+      "-d0", A.Set O.d0, help_d0;
+      "-d1", A.Set O.d1, help_d1;
+      "-d2", A.Set O.d2, help_d2;
+      "-e1", A.Set O.e1, help_e1;
+      "-e2", A.Set O.e2, help_e2;
+      "-p0", A.Set O.p0, help_p0;
+      "-p1", A.Set O.p1, help_p1;
+      "-p2", A.Set O.p2, help_p2;
    ] process_file help;
-   XU.write_hook hook !includes !tables 
+   XU.write_hook hook !includes !tables
 
 let _ = main ()
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma b/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma
index 589fc597c..a064c7e1f 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma
@@ -30,7 +30,7 @@ definition S2 ≝ λRR:relation4 genv lenv term term. λRS:relation term. λRP,C
                 ∀G,L,Vs. all … (RP G L) Vs →
                 ∀T. 𝐒❪T❫ → nf RR RS G L T → C G L (ⒶVs.T).
 
-(* Note: this generalizes Tait's ii *)
+(* Note: this generalizes Tait's ii, or Girard's CR3 *)
 definition S3 ≝ λC:candidate.
                 ∀a,G,L,Vs,V,T,W.
                 C G L (ⒶVs.ⓓ[a]ⓝW.V.T) → C G L (ⒶVs.ⓐV.ⓛ[a]W.T).