From 6bfdcdaf50cc3e5ca25079cd4006aeefac73c8c2 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 19 Feb 2017 15:55:59 +0000
Subject: [PATCH] - one annotation added - web page updated

---
 .../contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma    | 1 +
 .../matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml  | 5 ++++-
 .../matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl  | 3 ++-
 3 files changed, 7 insertions(+), 2 deletions(-)

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 6b5dfef44..4493ae7af 100644
--- 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 9f80ad898..b8c48ab9b 100644
--- 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 4d35bf981..a7fc0d856 100644
--- 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" *] 
           }
         ]        
      }
-- 
2.39.2