aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-07-28 10:18:08 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-07-29 01:36:42 +0200
commit0dac9618c695a345f82ee302b205217fff29be29 (patch)
tree6ce11d67daedf8ffe391df3e9ca9c3a7e899215f
parent0bc09220172b02c83eeba15350c26bd64cf0aa46 (diff)
Fixing some English misspelling.
-rw-r--r--kernel/cbytegen.ml22
-rw-r--r--kernel/cemitcodes.ml14
-rw-r--r--kernel/cemitcodes.mli2
-rw-r--r--kernel/csymtable.ml2
-rw-r--r--kernel/nativecode.ml2
-rw-r--r--kernel/nativelambda.ml6
-rw-r--r--kernel/nativelambda.mli2
7 files changed, 25 insertions, 25 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index d5435f0c3..3462694d6 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -524,14 +524,14 @@ let rec compile_fv reloc l sz cont =
(* Compiling constants *)
-let rec get_allias env (kn,u as p) =
+let rec get_alias env (kn,u as p) =
let cb = lookup_constant kn env in
let tps = cb.const_body_code in
match tps with
| None -> p
| Some tps ->
(match Cemitcodes.force tps with
- | BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u')
+ | BCalias (kn',u') -> get_alias env (kn', Univ.subst_instance_instance u u')
| _ -> p)
(* Compiling expressions *)
@@ -756,10 +756,10 @@ and compile_const =
(mkConstU (kn,u)) reloc args sz cont
with Not_found ->
if Int.equal nargs 0 then
- Kgetglobal (get_allias !global_env (kn, u)) :: cont
+ Kgetglobal (get_alias !global_env (kn, u)) :: cont
else
comp_app (fun _ _ _ cont ->
- Kgetglobal (get_allias !global_env (kn,u)) :: cont)
+ Kgetglobal (get_alias !global_env (kn,u)) :: cont)
compile_constr reloc () args sz cont
let compile fail_on_error env c =
@@ -797,14 +797,14 @@ let compile_constant_body fail_on_error env = function
| Const (kn',u) ->
(* we use the canonical name of the constant*)
let con= constant_of_kn (canonical_con kn') in
- Some (BCallias (get_allias env (con,u)))
+ Some (BCalias (get_alias env (con,u)))
| _ ->
let res = compile fail_on_error env body in
Option.map (fun x -> BCdefined (to_memory x)) res
(* Shortcut of the previous function used during module strengthening *)
-let compile_alias (kn,u) = BCallias (constant_of_kn (canonical_con kn), u)
+let compile_alias (kn,u) = BCalias (constant_of_kn (canonical_con kn), u)
(* spiwack: additional function which allow different part of compilation of the
31-bit integers *)
@@ -867,7 +867,7 @@ let op2_compilation op =
Kareconst(2, else_lbl):: Kacc 0:: Kpop 1::
op:: Kreturn 0:: Klabel else_lbl::
(* works as comp_app with nargs = 2 and tailcall cont [Kreturn 0]*)
- (*Kgetglobal (get_allias !global_env kn):: *)
+ (*Kgetglobal (get_alias !global_env kn):: *)
normal::
Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *)
in
@@ -886,7 +886,7 @@ let op2_compilation op =
(*Kaddint31::escape::Klabel else_lbl::Kpush::*)
(op::escape::Klabel else_lbl::Kpush::
(* works as comp_app with nargs = 2 and non-tailcall cont*)
- (*Kgetglobal (get_allias !global_env kn):: *)
+ (*Kgetglobal (get_alias !global_env kn):: *)
normal::
Kapply 2::labeled_cont)))
else if nargs=0 then
@@ -900,7 +900,7 @@ let op2_compilation op =
1/ checks if all the arguments are constants (i.e. non-block values)
2/ if they are, uses the "op" instruction to execute
3/ if at least one is not, branches to the normal behavior:
- Kgetglobal (get_allias !global_env kn) *)
+ Kgetglobal (get_alias !global_env kn) *)
let op_compilation n op =
let code_construct kn cont =
let f_cont =
@@ -908,7 +908,7 @@ let op_compilation n op =
Kareconst(n, else_lbl):: Kacc 0:: Kpop 1::
op:: Kreturn 0:: Klabel else_lbl::
(* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*)
- Kgetglobal (get_allias !global_env kn)::
+ Kgetglobal (get_alias !global_env kn)::
Kappterm(n, n):: [] (* = discard_dead_code [Kreturn 0] *)
in
let lbl = Label.create () in
@@ -926,7 +926,7 @@ let op_compilation n op =
(*Kaddint31::escape::Klabel else_lbl::Kpush::*)
(op::escape::Klabel else_lbl::Kpush::
(* works as comp_app with nargs = n and non-tailcall cont*)
- Kgetglobal (get_allias !global_env kn)::
+ Kgetglobal (get_alias !global_env kn)::
Kapply n::labeled_cont)))
else if Int.equal nargs 0 then
code_construct kn cont
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 6dbfbe9cc..9b275cb6c 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -328,36 +328,36 @@ let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
type body_code =
| BCdefined of to_patch
- | BCallias of pconstant
+ | BCalias of pconstant
| BCconstant
type to_patch_substituted =
| PBCdefined of to_patch substituted
-| PBCallias of pconstant substituted
+| PBCalias of pconstant substituted
| PBCconstant
let from_val = function
| BCdefined tp -> PBCdefined (from_val tp)
-| BCallias cu -> PBCallias (from_val cu)
+| BCalias cu -> PBCalias (from_val cu)
| BCconstant -> PBCconstant
let force = function
| PBCdefined tp -> BCdefined (force subst_to_patch tp)
-| PBCallias cu -> BCallias (force subst_pconstant cu)
+| PBCalias cu -> BCalias (force subst_pconstant cu)
| PBCconstant -> BCconstant
let subst_to_patch_subst s = function
| PBCdefined tp -> PBCdefined (subst_substituted s tp)
-| PBCallias cu -> PBCallias (subst_substituted s cu)
+| PBCalias cu -> PBCalias (subst_substituted s cu)
| PBCconstant -> PBCconstant
let repr_body_code = function
| PBCdefined tp ->
let (s, tp) = repr_substituted tp in
(s, BCdefined tp)
-| PBCallias cu ->
+| PBCalias cu ->
let (s, cu) = repr_substituted cu in
- (s, BCallias cu)
+ (s, BCalias cu)
| PBCconstant -> (None, BCconstant)
let to_memory (init_code, fun_code, fv) =
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index cec901306..54b92b912 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -25,7 +25,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
type body_code =
| BCdefined of to_patch
- | BCallias of constant Univ.puniverses
+ | BCalias of constant Univ.puniverses
| BCconstant
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 8fd90ec36..b3f0ba5b5 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -163,7 +163,7 @@ let rec slot_for_getglobal env (kn,u) =
let v = eval_to_patch env (code,pl,fv) in
set_global v
else set_global (val_of_constant (kn,u))
- | BCallias kn' -> slot_for_getglobal env kn'
+ | BCalias kn' -> slot_for_getglobal env kn'
| BCconstant -> set_global (val_of_constant (kn,u)) in
(*Pp.msgnl(str"value stored at: "++int pos);*)
rk := Some (Ephemeron.create pos);
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 90c437bbf..687b740f6 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2012,7 +2012,7 @@ let rec compile_deps env sigma prefix ~interactive init t =
match kind_of_term t with
| Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind
| Const c ->
- let c,u = get_allias env c in
+ let c,u = get_alias env c in
let cb,(nameref,_) = lookup_constant_key c env in
let (_, (_, const_updates)) = init in
if is_code_loaded ~interactive nameref
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 383f81029..cb08b5058 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -373,13 +373,13 @@ let makeblock env cn u tag args =
(* Translation of constants *)
-let rec get_allias env (kn, u as p) =
+let rec get_alias env (kn, u as p) =
let tps = (lookup_constant kn env).const_body_code in
match tps with
| None -> p
| Some tps ->
match Cemitcodes.force tps with
- | Cemitcodes.BCallias kn' -> get_allias env kn'
+ | Cemitcodes.BCalias kn' -> get_alias env kn'
| _ -> p
(*i Global environment *)
@@ -651,7 +651,7 @@ let rec lambda_of_constr env sigma c =
and lambda_of_app env sigma f args =
match kind_of_term f with
| Const (kn,u as c) ->
- let kn,u = get_allias !global_env c in
+ let kn,u = get_alias !global_env c in
let cb = lookup_constant kn !global_env in
(try
let prefix = get_const_prefix !global_env kn in
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index ccf2888b5..3b6fafbbc 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -26,7 +26,7 @@ val mk_lazy : lambda -> lambda
val get_mind_prefix : env -> mutual_inductive -> string
-val get_allias : env -> pconstant -> pconstant
+val get_alias : env -> pconstant -> pconstant
val lambda_of_constr : env -> evars -> Constr.constr -> lambda