Fix IH not appearing with pattern cast mismatch

Author: Negabinary

src/language/proof/MatchExp.re

@@ -265,6 +265,8 @@ and match_pat = (pat_r: Pat.t, pat: Pat.t): option(alphas) =>
   | (Projector(_, p1), _) => match_pat(p1, pat)
   | (_, Parens(p2))
   | (_, Projector(_, p2)) => match_pat(pat_r, p2)
+  | (Asc(p1, _), _) => match_pat(p1, pat)
+  | (_, Asc(p2, _)) => match_pat(pat_r, p2)
   | (Invalid(x), Invalid(y)) when x == y => Some([])
   | (Invalid(_), _) => None
   | (EmptyHole, EmptyHole) => Some([])
@@ -319,11 +321,6 @@ and match_pat = (pat_r: Pat.t, pat: Pat.t): option(alphas) =>
     let* alphas2 = match_pat(x2, y2);
     Some(alphas1 @ alphas2);
   | (Ap(_, _), _) => None
-  | (Asc(x, t1), Asc(y, t2)) =>
-    let* alphas1 = match_pat(x, y);
-    let* () = match_typ(t1, t2);
-    Some(alphas1);
-  | (Asc(_, _), _) => None
   | (Label(l1), Label(l2)) when l1 == l2 => Some([])
   | (Label(_), _) => None
   | (TupLabel({term: ExplicitNonlabel, _}, pat_r), _) =>

src/util/StringUtil.re

@@ -180,14 +180,5 @@ let subseq_search = (s: string, sub: string): bool => {
       );
     };
 
-  print_endline(
-    "Subseq search: "
-    ++ sub
-    ++ " in "
-    ++ s
-    ++ "returns"
-    ++ string_of_bool(search(0, 0)),
-  );
-
   search(0, 0);
 };