diff options
Diffstat (limited to 'kernel/mod_subst.mli')
| -rw-r--r-- | kernel/mod_subst.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 89491e2f91..0a3220293b 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -8,7 +8,7 @@ (*i $Id$ i*) -(*s Mod_subst *) +(*s [Mod_subst] *) open Names open Term |