aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssrmatching
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssrmatching')
-rw-r--r--plugins/ssrmatching/ssrmatching.ml42
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 60c199bf5..f146fbb11 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -435,8 +435,6 @@ let isRigid c = match kind_of_term c with
| Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true
| _ -> false
-exception UndefPat
-
let hole_var = mkVar (id_of_string "_")
let pr_constr_pat c0 =
let rec wipe_evar c =