aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/constr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/constr.ml')
-rw-r--r--kernel/constr.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index e2630c3f0..49e17d74d 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -124,7 +124,7 @@ type types = constr
(* Term constructors *)
(*********************)
-(* Constructs a DeBrujin index with number n *)
+(* Constructs a DeBruijn index with number n *)
let rels =
[|Rel 1;Rel 2;Rel 3;Rel 4;Rel 5;Rel 6;Rel 7; Rel 8;
Rel 9;Rel 10;Rel 11;Rel 12;Rel 13;Rel 14;Rel 15; Rel 16|]