aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrexpr_ops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrexpr_ops.mli')
-rw-r--r--interp/constrexpr_ops.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index d51576c04..0ff51b060 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -36,7 +36,6 @@ val binder_kind_eq : binder_kind -> binder_kind -> bool
val constr_loc : constr_expr -> Loc.t option
val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t option
-val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t option
val local_binders_loc : local_binder_expr list -> Loc.t option
(** {6 Constructors}*)