diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 15 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 6 |
2 files changed, 16 insertions, 5 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f72712cc8e..d1ca1a52fa 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -166,12 +166,11 @@ let execute_type env constr = let (j,cst) = execute env constr in (type_judgment env Evd.empty j, cst) +(* Renaming for the following. *) -(* Exported machines. *) +let safe_infer = execute -let safe_infer env constr = execute env constr - -let safe_infer_type env constr = execute_type env constr +let safe_infer_type = execute_type (* Typing of several terms. *) @@ -471,3 +470,11 @@ let import = import let env_of_safe_env e = e +(* Exported typing functions *) + +let typing env c = + let (j,cst) = safe_infer env c in + let _ = add_constraints cst env in + j + +let typing_in_unsafe_env = typing diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 4f94b904e3..04fbe21bb1 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -69,7 +69,7 @@ val import : compiled_env -> safe_environment -> safe_environment val env_of_safe_env : safe_environment -> env -(*s Typing judgments without modifying the global safe env - used in minicoq *) +(*s Typing judgments *) type judgment @@ -78,3 +78,7 @@ val j_type : judgment -> constr val safe_infer : safe_environment -> constr -> judgment * constraints +val typing : safe_environment -> constr -> judgment +val typing_in_unsafe_env : env -> constr -> judgment + + |