- minor corrections

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma
index 1e0ae189aa896377edaee75c02bf58d030daacf7..184716b90d3601ace5da07eef77481169ab1ba0e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma
@@ -14,9 +14,9 @@
 
 include "basic_2/relocation/drops.ma".
 
-(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************)
+(* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
 
-(* Properties on context sensitive equivalence for terms ********************)
+(* Properties with context-sensitive equivalence for terms ******************)
 
 lemma ceq_lift: d_liftable2 ceq.
 /2 width=3 by ex2_intro/ qed-.