Fix for bug 5507. Mispelt de Bruijn.

6 files changed, 11 insertions, 11 deletions

diff --git a/dev/doc/cic.dtd b/dev/doc/cic.dtd
index f2314e224..7a9d7eb1e 100644
--- a/dev/doc/cic.dtd
+++ b/dev/doc/cic.dtd
@@ -125,7 +125,7 @@
           id     ID     #REQUIRED
           sort   %sort; #REQUIRED>
 
-<!-- The substitutions are ordered by increasing DeBrujin  -->
+<!-- The substitutions are ordered by increasing DeBruijn  -->
 <!-- index. An empty substitution means that that index is -->
 <!-- not accessible.                                       -->
 <!ELEMENT META (substitution*)>
diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex
index 797b0aded..c55b3775c 100644
--- a/doc/refman/RefMan-tus.tex
+++ b/doc/refman/RefMan-tus.tex
@@ -299,7 +299,7 @@ vector of terms $vt$.
 \end{itemize}
 
 In this meta-language, bound variables are represented using the
-so-called deBrujin's indexes. In this representation, an occurrence of
+so-called deBruijn's indexes. In this representation, an occurrence of
 a bound variable is denoted by an integer, meaning the number of
 binders that must be traversed to reach its own
 binder\footnote{Actually, $(\texttt{Rel}\;n)$ means that $(n-1)$ binders
@@ -482,7 +482,7 @@ following constructor functions:
 
 \begin{description}
 \fun{val Term.mkRel          : int -> constr}
-    {$(\texttt{mkRel}\;n)$ represents deBrujin's index $n$.}
+    {$(\texttt{mkRel}\;n)$ represents deBruijn's index $n$.}
 
 \fun{val Term.mkVar : identifier -> constr} 
     {$(\texttt{mkVar}\;id)$
@@ -545,7 +545,7 @@ following constructor functions:
 
 \fun{val Term.mkProd : name ->constr ->constr -> constr}
     {$(\texttt{mkProd}\;x\;A\;B)$ represents the product $(x:A)B$.
-     The free ocurrences of $x$ in $B$ are represented by deBrujin's
+     The free ocurrences of $x$ in $B$ are represented by deBruijn's
      indexes.}
 
 \fun{val Term.mkNamedProd : identifier -> constr -> constr -> constr}
@@ -553,14 +553,14 @@ following constructor functions:
      but the bound occurrences of $x$ in $B$ are denoted by 
      the identifier $(\texttt{mkVar}\;x)$. The function automatically 
      changes each occurrences of this identifier into the corresponding 
-     deBrujin's index.}
+     deBruijn's index.}
 
 \fun{val Term.mkArrow : constr -> constr -> constr}
     {$(\texttt{arrow}\;A\;B)$ represents the type $(A\rightarrow B)$.}
 
 \fun{val Term.mkLambda       : name -> constr -> constr -> constr}
     {$(\texttt{mkLambda}\;x\;A\;b)$ represents the lambda abstraction 
-     $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by deBrujin's
+     $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by deBruijn's
      indexes.}
 
 \fun{val Term.mkNamedLambda : identifier -> constr -> constr -> constr}
@@ -666,7 +666,7 @@ use the primitive \textsl{Case} described in Chapter \ref{Cic}
 \item Restoring type coercions and synthesizing the implicit arguments
 (the one denoted by question marks in
 {\Coq} syntax: see Section~\ref{Coercions}).
-\item Transforming the named bound variables into deBrujin's indexes.
+\item Transforming the named bound variables into deBruijn's indexes.
 \item Classifying the global names into the different classes of
 constants (defined constants, constructors, inductive types, etc).
 \end{enumerate}
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|]
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 700c235e6..d90afea8f 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 e5a681375..7c6136f08 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 a9bb67705..623d2c8a6 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 *)