]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/coq-contribs/LAMBDA-TYPES/fsubst0_defs.v
ocaml 3.09 transition
[helm.git] / helm / coq-contribs / LAMBDA-TYPES / fsubst0_defs.v
index c7382bf207113dbe0b7b7c976b9dc38681ba7114..fa940493680928412a90bffc781e0a3ac092a4c3 100644 (file)
@@ -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"