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