advances in the theory of drops, lexs, and frees ...

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
index d89370b417b0b084e28e6094223623921dd46b1b..8140a5d31091fcb23900b7c69d3a5c8929f9d591 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
@@ -16,7 +16,7 @@ include "ground_2/relocation/rtmap_sle.ma".
 include "basic_2/notation/relations/relationstar_5.ma".
 include "basic_2/grammar/lenv.ma".
 
-(* GENERAL ENTRYWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
+(* GENERAL ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
 
 definition relation5 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0]
 ≝ λA,B,C,D,E.A→B→C→D→E→Prop.