update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / unwind / unwind_gen_structure.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
index d8a44810cf3a92f9619a5fba295da00e234ea933..5c92a9af5a364189d99d17b24a6cc7554b6c6710 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
@@ -19,9 +19,9 @@ include "delayed_updating/syntax/path_proper.ma".
 include "ground/xoa/ex_4_2.ma".
 include "ground/xoa/ex_3_2.ma".
 
-(* GENERIC UNWIND FOR PATH *************************************************)
+(* GENERIC UNWIND FOR PATH **************************************************)
 
-(* Basic constructions with structure **************************************)
+(* Basic constructions with structure ***************************************)
 
 lemma structure_unwind_gen (p) (f):
       ⊗p = ⊗◆[f]p.