diff options
author | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-05-01 17:48:57 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2017-05-01 17:48:57 +0200 |
commit | d0252cac3167ef1e5cd26c1b9b40aea06d343413 (patch) | |
tree | 9748fb6a7260592a1e0baca9da37c22d400ee51d /kernel | |
parent | 5365971dfdf4136586527aa4f4c85fbfebeee0bd (diff) |
More consistent writing of de Bruijn.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/constr.ml | 2 | ||||
-rw-r--r-- | kernel/constr.mli | 2 | ||||
-rw-r--r-- | kernel/nativeconv.ml | 2 | ||||
-rw-r--r-- | kernel/term.ml | 2 | ||||
-rw-r--r-- | kernel/term.mli | 2 | ||||
-rw-r--r-- | kernel/vars.ml | 2 | ||||
-rw-r--r-- | kernel/vars.mli | 4 |
7 files changed, 8 insertions, 8 deletions
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] *) |