aboutsummaryrefslogtreecommitdiff
path: root/interp/constrexpr_ops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrexpr_ops.ml')
-rw-r--r--interp/constrexpr_ops.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 7bc5d090b4..95a0039b0a 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -293,9 +293,6 @@ let ids_of_pattern_list =
(List.fold_left (cases_pattern_fold_names Id.Set.add))
Id.Set.empty
-let ids_of_cases_indtype p =
- cases_pattern_fold_names Id.Set.add Id.Set.empty p
-
let ids_of_cases_tomatch tms =
List.fold_right
(fun (_, ona, indnal) l ->