diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-01-12 13:50:50 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-01-12 13:50:50 +0100 |
| commit | e99e4006368fab3818812c6194d54465746c4566 (patch) | |
| tree | ab1e658475cb1e518e1611b58e0d64ee3cf21b32 /kernel/safe_typing.ml | |
| parent | 4b8cd99705596052b7b45f29c248c9d02875ccdc (diff) | |
Fix a few typos.
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 27f94972a..0915ef577 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -190,7 +190,7 @@ let set_type_in_type senv = (** {6 Stm machinery } *) -let get_opauqe_body env cbo = +let get_opaque_body env cbo = match cbo.const_body with | Undef _ -> assert false | Def _ -> `Nothing @@ -201,12 +201,12 @@ let get_opauqe_body env cbo = let sideff_of_con env c = let cbo = Environ.lookup_constant c env.env in - SEsubproof (c, cbo, get_opauqe_body env.env cbo) + SEsubproof (c, cbo, get_opaque_body env.env cbo) let sideff_of_scheme kind env cl = SEscheme( List.map (fun (i,c) -> let cbo = Environ.lookup_constant c env.env in - i, c, cbo, get_opauqe_body env.env cbo) cl, + i, c, cbo, get_opaque_body env.env cbo) cl, kind) let env_of_safe_env senv = senv.env |