From 5365971dfdf4136586527aa4f4c85fbfebeee0bd Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 1 May 2017 15:00:56 +0200
Subject: Fix for bug 5507. Mispelt de Bruijn.

---
 kernel/constr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/constr.ml')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index e2630c3f08..49e17d74d5 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|]
-- 
cgit v1.2.3