aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/vars.ml
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-05-01 17:48:57 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-05-01 17:48:57 +0200
commitd0252cac3167ef1e5cd26c1b9b40aea06d343413 (patch)
tree9748fb6a7260592a1e0baca9da37c22d400ee51d /kernel/vars.ml
parent5365971dfdf4136586527aa4f4c85fbfebeee0bd (diff)
More consistent writing of de Bruijn.
Diffstat (limited to 'kernel/vars.ml')
-rw-r--r--kernel/vars.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 4affb5f9f..f1c0a4f08 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -27,7 +27,7 @@ let closedn n c =
in
try closed_rec n c; true with LocalOccur -> false
-(* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
+(* [closed0 M] is true iff [M] is a (de Bruijn) closed term *)
let closed0 c = closedn 0 c