- minor corrections

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / freq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/freq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/freq.ma
index c9a3353488750e4142e3af6a09076b8773f507de..0f3868536fc5952bd3a1b67cf83db82a2e835e87 100644 (file)
--- 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