Merge PR#596: Fix for bug 5507. Mispelt de Bruijn.

7 files changed, 8 insertions, 8 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index e2630c3f08..ae58fd068b 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 de Bruijn 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..e0954160f9 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 de Bruijn index (DB indices begin at 1) *)
 val mkRel : int -> constr
 
 (** Constructs a Variable *)
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 3c0afe3805..3593d94c2c 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -141,7 +141,7 @@ let native_conv_gen pb sigma env univs t1 t2 =
         let t1 = Sys.time () in
         let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
         if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
-        (* TODO change 0 when we can have deBruijn *)
+        (* TODO change 0 when we can have de Bruijn *)
         fst (conv_val env pb 0 !rt1 !rt2 univs)
       end
   | _ -> anomaly (Pp.str "Compilation failure") 
diff --git a/kernel/term.ml b/kernel/term.ml
index e5a681375d..03562d9f31 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 de Bruijn 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..241ef322fa 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 de Bruijn index *)
 val destRel : constr -> int
 
 (** Destructs an existential variable *)
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 4affb5f9fb..f1c0a4f08a 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
 
diff --git a/kernel/vars.mli b/kernel/vars.mli
index adeac422e0..df5c55118f 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -11,10 +11,10 @@ open Constr
 
 (** {6 Occur checks } *)
 
-(** [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *)
+(** [closedn n M] is true iff [M] is a (de Bruijn) closed term under n binders *)
 val closedn : int -> constr -> bool
 
-(** [closed0 M] is true iff [M] is a (deBruijn) closed term *)
+(** [closed0 M] is true iff [M] is a (de Bruijn) closed term *)
 val closed0 : constr -> bool
 
 (** [noccurn n M] returns true iff [Rel n] does NOT occur in term [M]  *)