aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/safe_typing.mli')
-rw-r--r--kernel/safe_typing.mli13
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*)
-