aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/vars.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/vars.mli')
-rw-r--r--kernel/vars.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/vars.mli b/kernel/vars.mli
index adeac422e..df5c55118 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -11,10 +11,10 @@ open Constr
(** {6 Occur checks } *)
-(** [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *)
+(** [closedn n M] is true iff [M] is a (de Bruijn) closed term under n binders *)
val closedn : int -> constr -> bool
-(** [closed0 M] is true iff [M] is a (deBruijn) closed term *)
+(** [closed0 M] is true iff [M] is a (de Bruijn) closed term *)
val closed0 : constr -> bool
(** [noccurn n M] returns true iff [Rel n] does NOT occur in term [M] *)