X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Ffreq.ma;h=0f3868536fc5952bd3a1b67cf83db82a2e835e87;hb=d3636c8688ec08cc39eb7ce6c1918b25bbccc349;hp=c9a3353488750e4142e3af6a09076b8773f507de;hpb=7fff13721f6e7040e76faad31583b1cb86693d2c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/freq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/freq.ma
index c9a335348..0f3868536 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/freq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/freq.ma
@@ -17,7 +17,7 @@ include "basic_2/grammar/genv.ma".
 include "basic_2/relocation/frees_weight.ma".
 include "basic_2/relocation/frees_lreq.ma".
 
-(* LAZY EQUIVALENCE FOR CLOSURES ********************************************)
+(* RANGED EQUIVALENCE FOR CLOSURES ******************************************)
 
 inductive freq (G) (L1) (T): relation3 genv lenv term ≝
 | fleq_intro: ∀L2,f. L1 ⊢ 𝐅*⦃T⦄ ≡ f → L1 ≡[f] L2 → freq G L1 T G L2 T