aboutsummaryrefslogtreecommitdiff
path: root/interp/constrexpr_ops.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-05-19 10:48:30 +0200
committerPierre-Marie Pédrot2017-05-19 10:48:30 +0200
commit0a67131d9a63e26ea2ea85d9ed51d76d8464295e (patch)
tree980727a88f63908ce1f25f317e43126a0d3d0ad8 /interp/constrexpr_ops.mli
parent37e84b83739fec666264904bc06fd32b46b83140 (diff)
parent9f11adda4bff194a3c6a66d573ce7001d4399886 (diff)
Merge branch 'master' into ltac2-hooks
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 f6d97e107d..b547288e3f 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
val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t
-val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t
val local_binders_loc : local_binder_expr list -> Loc.t
(** {6 Constructors}*)