Fixing some English misspelling.

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