aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/safe_typing.ml')
-rw-r--r--kernel/safe_typing.ml7
1 files changed, 1 insertions, 6 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f424f79db..74e33cdfb 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -151,9 +151,4 @@ 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 = Typeops.typing