- one annotation added

- web page updated

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma
index 6b5dfef444291d3a02e502e66ed9269c6e841dc9..4493ae7af89d02aa535034317b32251a0ff3aae5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma
@@ -78,6 +78,7 @@ interpretation
 
 (* Basic properties *********************************************************)
 
+(* Note: this requires Ⓕ-slicing in cfun since b is unknown in d_liftable_1 *) 
 (* Note: this requires multiple relocation *)
 (* Basic 1: includes: sc3_lift *)
 (* Basic 2A1: includes: gcr_lift *)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
index 9f80ad898c82f3d04a1e652b5cc41de0c4370189..b8c48ab9bf25b74d04be9bd5906a91ab7c7127ab 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
@@ -34,6 +34,9 @@
 
    <subsection name="A2">Stage "A2": "Extending the Applicability Condition"</subsection>
 
+   <news class="alpha" date="2017 February 19.">
+         Generic candidates of reducibility.
+   </news>
    <news class="alpha" date="2017 January 17.">
          Confluence for parallel r-transition on referred entries of local environments.
    </news>
@@ -116,7 +119,7 @@
          for simply typed terms.
    </news>
    <news class="alpha" date="2012 January 27.">
-         Support for abstract candidates of reducibility.
+         Generic candidates of reducibility.
    </news>
    <news class="alpha" date="2011 September 21.">
          Confluence for context-sensitive parallel reduction on terms.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 4d35bf98147944907595236d0f04e62f578edae7..a7fc0d856ba32b0fa440ff5f1a17671d104d4113 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -126,7 +126,8 @@ table {
         ]
         [ { "generic reducibility" * } {
              [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drop" + "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ]        
-             [ "gcp" "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
+             [ "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
+             [ "gcp" *] 
           }
         ]        
      }