From 534e02c863b5a571c6d8bd65cf72a4ce92fe4701 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 31 Dec 2018 19:58:32 +0000
Subject: Last rewrite reordering needs more typechecking

---
 src/rewrites.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/rewrites.ml b/src/rewrites.ml
index 3cd89b89..7ccff222 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -5064,10 +5064,11 @@ let rewrite_defs_coq = [
   ("trivial_sizeof", rewrite_trivial_sizeof);
   ("sizeof", rewrite_sizeof);
   ("early_return", rewrite_defs_early_return);
-  ("make_cases_exhaustive", MakeExhaustive.rewrite);
   (* merge funcls before adding the measure argument so that it doesn't
      disappear into an internal pattern match *)
   ("merge function clauses", merge_funcls);
+  ("recheck_defs", recheck_defs);
+  ("make_cases_exhaustive", MakeExhaustive.rewrite);
   ("rewrite_explicit_measure", rewrite_explicit_measure);
   ("recheck_defs_without_effects", recheck_defs_without_effects);
   ("fix_val_specs", rewrite_fix_val_specs);
-- 
cgit v1.2.3