aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/loc.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/loc.ml')
-rw-r--r--lib/loc.ml6
1 files changed, 0 insertions, 6 deletions
diff --git a/lib/loc.ml b/lib/loc.ml
index 4a935a9d9..2cf4d3960 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -84,9 +84,3 @@ let raise ?loc e =
let info = Exninfo.add Exninfo.null location loc in
Exninfo.iraise (e, info)
-(** Deprecated *)
-let located_fold_left f x (_,a) = f x a
-let located_iter2 f (_,a) (_,b) = f a b
-let down_located f (_,a) = f a
-
-