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 +-
 kernel/constr.mli | 2 +-
 kernel/term.ml    | 2 +-
 kernel/term.mli   | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel')

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|]
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 700c235e6a..d90afea8f2 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -70,7 +70,7 @@ type types = constr
 
 (** {6 Term constructors. } *)
 
-(** Constructs a DeBrujin index (DB indices begin at 1) *)
+(** Constructs a DeBruijn index (DB indices begin at 1) *)
 val mkRel : int -> constr
 
 (** Constructs a Variable *)
diff --git a/kernel/term.ml b/kernel/term.ml
index e5a681375d..7c6136f088 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -169,7 +169,7 @@ let hcons_types = Constr.hcons
 
 exception DestKO
 
-(* Destructs a DeBrujin index *)
+(* Destructs a DeBruijn index *)
 let destRel c = match kind_of_term c with
   | Rel n -> n
   | _ -> raise DestKO
diff --git a/kernel/term.mli b/kernel/term.mli
index a9bb677050..623d2c8a6b 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -127,7 +127,7 @@ val is_small : sorts -> bool
 
 exception DestKO
 
-(** Destructs a DeBrujin index *)
+(** Destructs a DeBruijn index *)
 val destRel : constr -> int
 
 (** Destructs an existential variable *)
-- 
cgit v1.2.3