aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/environ.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/environ.mli')
-rw-r--r--kernel/environ.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 5be23b490..20027d32a 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -46,7 +46,7 @@ val engagement : env -> engagement option
val empty_context : env -> bool
(************************************************************************)
-(*s Context of de Bruijn variables (rel_context) *)
+(*s Context of de Bruijn variables ([rel_context]) *)
val push_rel : rel_declaration -> env -> env
val push_rel_context : rel_context -> env -> env
val push_rec_types : rec_declaration -> env -> env