aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-05-01 17:48:57 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2017-05-01 17:48:57 +0200
commitd0252cac3167ef1e5cd26c1b9b40aea06d343413 (patch)
tree9748fb6a7260592a1e0baca9da37c22d400ee51d
parent5365971dfdf4136586527aa4f4c85fbfebeee0bd (diff)
More consistent writing of de Bruijn.
-rw-r--r--checker/term.ml4
-rw-r--r--dev/doc/cic.dtd2
-rw-r--r--doc/RecTutorial/coqartmacros.tex2
-rw-r--r--doc/refman/RefMan-tus.tex18
-rw-r--r--engine/evarutil.ml2
-rw-r--r--kernel/constr.ml2
-rw-r--r--kernel/constr.mli2
-rw-r--r--kernel/nativeconv.ml2
-rw-r--r--kernel/term.ml2
-rw-r--r--kernel/term.mli2
-rw-r--r--kernel/vars.ml2
-rw-r--r--kernel/vars.mli4
-rw-r--r--tactics/dnet.mli2
-rw-r--r--vernac/auto_ind_decl.ml4
-rw-r--r--vernac/obligations.ml6
15 files changed, 28 insertions, 28 deletions
diff --git a/checker/term.ml b/checker/term.ml
index 591348cb6..24e6008d3 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* This module instantiates the structure of generic deBruijn terms to Coq *)
+(* This module instantiates the structure of generic de Bruijn terms to Coq *)
open CErrors
open Util
@@ -94,7 +94,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 = closedn 0
diff --git a/dev/doc/cic.dtd b/dev/doc/cic.dtd
index 7a9d7eb1e..cc33efd48 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 DeBruijn -->
+<!-- The substitutions are ordered by increasing de Bruijn -->
<!-- index. An empty substitution means that that index is -->
<!-- not accessible. -->
<!ELEMENT META (substitution*)>
diff --git a/doc/RecTutorial/coqartmacros.tex b/doc/RecTutorial/coqartmacros.tex
index 2a2c21196..72d749269 100644
--- a/doc/RecTutorial/coqartmacros.tex
+++ b/doc/RecTutorial/coqartmacros.tex
@@ -149,7 +149,7 @@
\newcommand{\PicAbst}[3]{\begin{bundle}{\bf abst}\chunk{#1}\chunk{#2}\chunk{#3}%
\end{bundle}}
-% the same in DeBruijn form
+% the same in de Bruijn form
\newcommand{\PicDbj}[2]{\begin{bundle}{\bf abst}\chunk{#1}\chunk{#2}
\end{bundle}}
diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex
index c55b3775c..017de6d48 100644
--- a/doc/refman/RefMan-tus.tex
+++ b/doc/refman/RefMan-tus.tex
@@ -288,8 +288,8 @@ constructors:
\item $(\texttt{VAR}\;id)$, a reference to a global identifier called $id$;
\item $(\texttt{Rel}\;n)$, a bound variable, whose binder is the $nth$
binder up in the term;
-\item $\texttt{DLAM}\;(x,t)$, a deBruijn's binder on the term $t$;
-\item $\texttt{DLAMV}\;(x,vt)$, a deBruijn's binder on all the terms of
+\item $\texttt{DLAM}\;(x,t)$, a de Bruijn's binder on the term $t$;
+\item $\texttt{DLAMV}\;(x,vt)$, a de Bruijn's binder on all the terms of
the vector $vt$;
\item $(\texttt{DOP0}\;op)$, a unary operator $op$;
\item $\texttt{DOP2}\;(op,t_1,t_2)$, the application of a binary
@@ -299,7 +299,7 @@ vector of terms $vt$.
\end{itemize}
In this meta-language, bound variables are represented using the
-so-called deBruijn's indexes. In this representation, an occurrence of
+so-called de Bruijn'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
@@ -339,7 +339,7 @@ on the terms of the meta-language:
\fun{val Generic.dependent : 'op term -> 'op term -> bool}
{Returns true if the first term is a sub-term of the second.}
%\fun{val Generic.subst\_var : identifier -> 'op term -> 'op term}
-% { $(\texttt{subst\_var}\;id\;t)$ substitutes the deBruijn's index
+% { $(\texttt{subst\_var}\;id\;t)$ substitutes the de Bruijn's index
% associated to $id$ to every occurrence of the term
% $(\texttt{VAR}\;id)$ in $t$.}
\end{description}
@@ -482,7 +482,7 @@ following constructor functions:
\begin{description}
\fun{val Term.mkRel : int -> constr}
- {$(\texttt{mkRel}\;n)$ represents deBruijn's index $n$.}
+ {$(\texttt{mkRel}\;n)$ represents de Bruijn'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 deBruijn's
+ The free ocurrences of $x$ in $B$ are represented by de Bruijn'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
- deBruijn's index.}
+ de Bruijn'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 deBruijn's
+ $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by de Bruijn'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 deBruijn's indexes.
+\item Transforming the named bound variables into de Bruijn's indexes.
\item Classifying the global names into the different classes of
constants (defined constants, constructors, inductive types, etc).
\end{enumerate}
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 1624dc93e..22f93faa6 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -462,7 +462,7 @@ let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?nami
ev
(* This assumes an evar with identity instance and generalizes it over only
- the De Bruijn part of the context *)
+ the de Bruijn part of the context *)
let generalize_evar_over_rels sigma (ev,args) =
let open EConstr in
let evi = Evd.find sigma ev in
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 49e17d74d..ae58fd068 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -124,7 +124,7 @@ type types = constr
(* Term constructors *)
(*********************)
-(* Constructs a DeBruijn 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 d90afea8f..e0954160f 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -70,7 +70,7 @@ type types = constr
(** {6 Term constructors. } *)
-(** Constructs a DeBruijn 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 3c0afe380..3593d94c2 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 7c6136f08..03562d9f3 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
diff --git a/kernel/term.mli b/kernel/term.mli
index 623d2c8a6..241ef322f 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -127,7 +127,7 @@ val is_small : sorts -> bool
exception DestKO
-(** Destructs a DeBruijn 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 4affb5f9f..f1c0a4f08 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 adeac422e..df5c55118 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] *)
diff --git a/tactics/dnet.mli b/tactics/dnet.mli
index 9f29c60b6..565a916f8 100644
--- a/tactics/dnet.mli
+++ b/tactics/dnet.mli
@@ -26,7 +26,7 @@
distincts, or you'll get unexpected behaviours.
Warning 2: This structure is perfect, i.e. the set of candidates
- returned is equal to the set of solutions. Beware of DeBruijn
+ returned is equal to the set of solutions. Beware of de Bruijn
shifts and sorts subtyping though (which makes the comparison not
symmetric, see term_dnet.ml).
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index b9c4c6cc5..c91dcc505 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -95,7 +95,7 @@ let destruct_on_using c id =
let destruct_on_as c l =
destruct false None c (Some (dl,l)) None
-(* reconstruct the inductive with the correct deBruijn indexes *)
+(* reconstruct the inductive with the correct de Bruijn indexes *)
let mkFullInd (ind,u) n =
let mib = Global.lookup_mind (fst ind) in
let nparams = mib.mind_nparams in
@@ -174,7 +174,7 @@ let build_beq_scheme mode kn =
(* give a type A, this function tries to find the equality on A declared
previously *)
(* nlist = the number of args (A , B , ... )
- eqA = the deBruijn index of the first eq param
+ eqA = the de Bruijn index of the first eq param
ndx = how much to translate due to the 2nd Case
*)
let compute_A_equality rel_list nlist eqA ndx t =
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index ea2401b5c..e0520216b 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -8,7 +8,7 @@ open Declare
(**
- Get types of existentials ;
- Flatten dependency tree (prefix order) ;
- - Replace existentials by De Bruijn indices in term, applied to the right arguments ;
+ - Replace existentials by de Bruijn indices in term, applied to the right arguments ;
- Apply term prefixed by quantification on "existentials".
*)
@@ -51,7 +51,7 @@ type oblinfo =
ev_tac: unit Proofview.tactic option;
ev_deps: Int.Set.t }
-(** Substitute evar references in t using De Bruijn indices,
+(** Substitute evar references in t using de Bruijn indices,
where n binders were passed through. *)
let subst_evar_constr evs n idf t =
@@ -102,7 +102,7 @@ let subst_evar_constr evs n idf t =
t', !seen, !transparent
-(** Substitute variable references in t using De Bruijn indices,
+(** Substitute variable references in t using de Bruijn indices,
where n binders were passed through. *)
let subst_vars acc n t =
let var_index id = Util.List.index Id.equal id acc in