some notation renamed and fixed

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cir_append.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma
index 2f04611910838a2249c5256064596f7ba4bcefd8..efd097f8446d9cd27c086d72604ba0dfbec884f0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cir_append.ma
@@ -15,7 +15,7 @@
 include "basic_2/reduction/crr_append.ma".
 include "basic_2/reduction/cir.ma".
 
-(* CONTEXT-SENSITIVE IRREDUCIBLE TERMS **************************************)
+(* IRREDUCIBLE TERMS FOR CONTEXT-SENSITIVE REDUCTION ************************)
 
 (* Advanved properties ******************************************************)