X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fcsubst0_defs.v;h=046b1978cf2216204f2b6d1c4db08b28f1c4a642;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=8d1ff31dc936c9038dc1e0e155ab229e204f9c96;hpb=a8052b7482d5573eca2776ea11cb7a4b06236fbd;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/csubst0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/csubst0_defs.v
index 8d1ff31dc..046b1978c 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/csubst0_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/csubst0_defs.v
@@ -2,7 +2,7 @@ Require Export contexts_defs.
 Require Export subst0_defs.
 Require Export drop_defs.
 
-(*#* #caption "current axioms for strict substitution in contexts",
+(*#* #caption "axioms for strict substitution in contexts",
    "substituted tail item: second operand", 
    "substituted tail item: first operand", 
    "substituted tail item: both operands"