diff options
-rw-r--r-- | dev/doc/cic.dtd | 2 | ||||
-rw-r--r-- | doc/refman/RefMan-tus.tex | 12 | ||||
-rw-r--r-- | kernel/constr.ml | 2 | ||||
-rw-r--r-- | kernel/constr.mli | 2 | ||||
-rw-r--r-- | kernel/term.ml | 2 | ||||
-rw-r--r-- | kernel/term.mli | 2 |
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 *) |