diff options
Diffstat (limited to 'kernel/safe_typing.mli')
| -rw-r--r-- | kernel/safe_typing.mli | 6 |
1 files changed, 5 insertions, 1 deletions
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 + + |