- one annotation added

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / gcp_cr.ma

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 *)