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/term.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/term.ml')

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
-- 
cgit v1.2.3


From d0252cac3167ef1e5cd26c1b9b40aea06d343413 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 1 May 2017 17:48:57 +0200
Subject: More consistent writing of de Bruijn.

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

(limited to 'kernel/term.ml')

diff --git a/kernel/term.ml b/kernel/term.ml
index 7c6136f088..03562d9f31 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -169,7 +169,7 @@ let hcons_types = Constr.hcons
 
 exception DestKO
 
-(* Destructs a DeBruijn index *)
+(* Destructs a de Bruijn index *)
 let destRel c = match kind_of_term c with
   | Rel n -> n
   | _ -> raise DestKO
-- 
cgit v1.2.3