Coq: fix non-exhaustive pattern match failure in riscv duopod

1 files changed, 4 insertions, 1 deletions

diff --git a/src/rewrites.ml b/src/rewrites.ml
index 89b49043..ad0ed836 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -4935,11 +4935,14 @@ let rewrites_coq = [
     ("move_termination_measures", []);
     ("top_sort_defs", []);
     ("early_return", []);
+    (* We need to do the exhaustiveness check before merging, because it may
+       introduce new wildcard clauses *)
+    ("recheck_defs_without_effects", []);
+    ("make_cases_exhaustive", []);
     (* merge funcls before adding the measure argument so that it doesn't
      disappear into an internal pattern match *)
     ("merge_function_clauses", []);
     ("recheck_defs_without_effects", []);
-    ("make_cases_exhaustive", []);
     ("rewrite_explicit_measure", []);
     ("rewrite_loops_with_escape_effect", []);
     ("recheck_defs_without_effects", []);