diff options
Diffstat (limited to 'kernel/safe_typing.mli')
-rw-r--r-- | kernel/safe_typing.mli | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 90703ae96..4f94b904e 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -78,16 +78,3 @@ val j_type : judgment -> constr val safe_infer : safe_environment -> constr -> judgment * constraints -(*i For debug -val fix_machine : safe_environment -> constr -> judgment * constraints -val fix_machine_type : safe_environment -> constr -> types * constraints - -val unsafe_infer : safe_environment -> constr -> judgment * constraints -val unsafe_infer_type : safe_environment -> constr -> types * constraints - -val type_of : safe_environment -> constr -> constr - -val type_of_type : safe_environment -> constr -> constr -val unsafe_type_of : safe_environment -> constr -> constr -i*) - |