aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrexpr_ops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrexpr_ops.ml')
-rw-r--r--interp/constrexpr_ops.ml6
1 files changed, 0 insertions, 6 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index a592b4cff..542f9feaf 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -263,12 +263,6 @@ let cases_pattern_expr_loc = function
| CPatDelimiters (loc,_,_) -> loc
| CPatCast(loc,_,_) -> loc
-let raw_cases_pattern_expr_loc = function
- | RCPatAlias (loc,_,_) -> loc
- | RCPatCstr (loc,_,_,_) -> loc
- | RCPatAtom (loc,_) -> loc
- | RCPatOr (loc,_) -> loc
-
let local_binder_loc = function
| CLocalAssum ((loc,_)::_,_,t)
| CLocalDef ((loc,_),t,None) -> Loc.merge loc (constr_loc t)