diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/coq_memory.c | 2 | ||||
| -rw-r--r-- | kernel/cClosure.ml | 4 | ||||
| -rw-r--r-- | kernel/cClosure.mli | 2 | ||||
| -rw-r--r-- | kernel/cbytegen.ml | 2 | ||||
| -rw-r--r-- | kernel/constr.mli | 2 | ||||
| -rw-r--r-- | kernel/declarations.ml | 4 | ||||
| -rw-r--r-- | kernel/inductive.ml | 2 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 2 | ||||
| -rw-r--r-- | kernel/modops.ml | 2 | ||||
| -rw-r--r-- | kernel/uint63.mli | 2 | ||||
| -rw-r--r-- | kernel/univ.ml | 2 | ||||
| -rw-r--r-- | kernel/univ.mli | 2 | ||||
| -rw-r--r-- | kernel/vmvalues.ml | 2 |
13 files changed, 15 insertions, 15 deletions
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 542a05fd25..a1c49bee95 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -105,7 +105,7 @@ value init_coq_vm(value unit) /* ML */ init_coq_interpreter(); /* Some predefined pointer code. - * It is typically contained in accumlator blocks whose tag is 0 and thus + * It is typically contained in accumulator blocks whose tag is 0 and thus * scanned by the GC, so make it look like an OCaml block. */ value accu_block = (value) coq_stat_alloc(2 * sizeof(value)); Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \ diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 95f88c0306..fc7d1a54f2 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -226,7 +226,7 @@ let unfold_red kn = * this constant or abstraction. * * i_tab is the cache table of the results * - * ref_value_cache searchs in the tab, otherwise uses i_repr to + * ref_value_cache searches in the tab, otherwise uses i_repr to * compute the result and store it in the table. If the constant can't * be unfolded, returns None, but does not store this failure. * This * doesn't take the RESET into account. You mustn't keep such a table @@ -645,7 +645,7 @@ and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with and comp_subs el s = Esubst.lift_subst (fun el c -> lazy (to_constr el c)) el s -(* This function defines the correspondance between constr and +(* This function defines the correspondence between constr and fconstr. When we find a closure whose substitution is the identity, then we directly return the constr to avoid possibly huge reallocation. *) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 1a790eaed6..60185464c5 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -200,7 +200,7 @@ val whd_val : clos_infos -> clos_tab -> fconstr -> constr val whd_stack : clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack -(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding +(** [eta_expand_ind_stack env ind c s t] computes stacks corresponding to the conversion of the eta expansion of t, considered as an inhabitant of ind, and the Constructor c of this inductive type applied to arguments s. diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 69f004307d..90fbcb8ae3 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -386,7 +386,7 @@ let rec is_tailcall = function | Klabel _ :: c -> is_tailcall c | _ -> None -(* Extention of the continuation *) +(* Extension of the continuation *) (* Add a Kpop n instruction in front of a continuation *) let rec add_pop n = function diff --git a/kernel/constr.mli b/kernel/constr.mli index 7fc57cdb8a..aa5878c9d7 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -141,7 +141,7 @@ val mkRef : GlobRef.t Univ.puniverses -> constr [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] presented as describe in [ci]. - [p] stucture is [fun args x -> "return clause"] + [p] structure is [fun args x -> "return clause"] [ac]{^ ith} element is ith constructor case presented as {e lambda construct_args (without params). case_term } *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 36ee952099..860d19fe26 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -22,11 +22,11 @@ type engagement = set_predicativity (** {6 Representation of constants (Definition/Axiom) } *) (** Non-universe polymorphic mode polymorphism (Coq 8.2+): inductives - and constants hiding inductives are implicitely polymorphic when + and constants hiding inductives are implicitly polymorphic when applied to parameters, on the universes appearing in the whnf of their parameters and their conclusion, in a template style. - In truely universe polymorphic mode, we always use RegularArity. + In truly universe polymorphic mode, we always use RegularArity. *) type template_arity = { diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d9335d39b5..ca7086a3e4 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -166,7 +166,7 @@ let make_subst env = (* template, it is identity substitution otherwise (ie. when u is *) (* already in the domain of the substitution) [remember_subst] will *) (* update its image [x] by [sup x u] in order not to forget the *) - (* dependency in [u] that remains to be fullfilled. *) + (* dependency in [u] that remains to be fulfilled. *) make (remember_subst u subst) (sign, exp, []) | _sign, [], _ -> (* Uniform parameters are exhausted *) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 2de5faa6df..72393d0081 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -188,7 +188,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv = in let new_equiv = add_delta_resolver equiv new_mb.mod_delta in (* we propagate the new equality in the rest of the signature - with the identity substitution accompagned by the new resolver*) + with the identity substitution accompanied by the new resolver*) let id_subst = map_mp mp' mp' new_mb.mod_delta in let new_after = subst_structure id_subst after in before@(lab,SFBmodule new_mb')::new_after, new_equiv, cst diff --git a/kernel/modops.ml b/kernel/modops.ml index 4fdd7ab334..472fddb829 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -515,7 +515,7 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso = "Module M:=P." or "Module M. Include P. End M." We need to perform two operations to compute the body of M. - The first one is applying the substitution {P <- M} on the type of P - - The second one is strenghtening. *) + - The second one is strengthening. *) let strengthen_and_subst_mb mb mp include_b = match mb.mod_type with |NoFunctor struc -> diff --git a/kernel/uint63.mli b/kernel/uint63.mli index f25f24512d..93632da110 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -13,7 +13,7 @@ val of_uint : int -> t val hash : t -> int - (* convertion to a string *) + (* conversion to a string *) val to_string : t -> string val of_string : string -> t diff --git a/kernel/univ.ml b/kernel/univ.ml index b1bbc25fe6..2b88d6884d 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -726,7 +726,7 @@ let univ_level_rem u v min = | Some u' -> if Level.equal u u' then min else v | None -> List.filter (fun (l, n) -> not (Int.equal n 0 && Level.equal u l)) v -(* Is u mentionned in v (or equals to v) ? *) +(* Is u mentioned in v (or equals to v) ? *) (**********************************************************************) diff --git a/kernel/univ.mli b/kernel/univ.mli index db178c4bb0..ddb204dd52 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -163,7 +163,7 @@ val super : Universe.t -> Universe.t val universe_level : Universe.t -> Level.t option -(** [univ_level_mem l u] Is l is mentionned in u ? *) +(** [univ_level_mem l u] Is l is mentioned in u ? *) val univ_level_mem : Level.t -> Universe.t -> bool diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 777a207013..5e3a3c3347 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -12,7 +12,7 @@ open Univ open Constr (*******************************************) -(* Initalization of the abstract machine ***) +(* Initialization of the abstract machine ***) (* Necessary for [relaccu_tbl] *) (*******************************************) |