X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Ffsubst0_defs.v;h=fa940493680928412a90bffc781e0a3ac092a4c3;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=c7382bf207113dbe0b7b7c976b9dc38681ba7114;hpb=1ea21db6644417e6cd3c44c84915712a5321a37a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/fsubst0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/fsubst0_defs.v
index c7382bf20..fa9404936 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/fsubst0_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/fsubst0_defs.v
@@ -1,7 +1,7 @@
 Require Export subst0_defs.
 Require Export csubst0_defs.
 
-(*#* #caption "axioms for strict substitution in focalized terms",
+(*#* #caption "\\kern-1.2pt axioms for strict substitution in focalized terms",
    "substituted term part", 
    "substituted context part", 
    "substituted both parts"