diff options
| author | Hugo Herbelin | 2015-07-28 10:18:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-07-29 01:36:42 +0200 |
| commit | 0dac9618c695a345f82ee302b205217fff29be29 (patch) | |
| tree | 6ce11d67daedf8ffe391df3e9ca9c3a7e899215f /kernel/nativelambda.ml | |
| parent | 0bc09220172b02c83eeba15350c26bd64cf0aa46 (diff) | |
Fixing some English misspelling.
Diffstat (limited to 'kernel/nativelambda.ml')
| -rw-r--r-- | kernel/nativelambda.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 383f810295..cb08b5058f 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 |
