diff options
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/cbytegen.ml | 22 | ||||
-rw-r--r-- | kernel/cemitcodes.ml | 14 | ||||
-rw-r--r-- | kernel/cemitcodes.mli | 2 | ||||
-rw-r--r-- | kernel/csymtable.ml | 2 | ||||
-rw-r--r-- | kernel/nativecode.ml | 2 | ||||
-rw-r--r-- | kernel/nativelambda.ml | 6 | ||||
-rw-r--r-- | kernel/nativelambda.mli | 2 |
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 |