From dccff374cc4ff0d2ac9737a1abd1907118af6456 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 31 Dec 2018 11:01:54 +0000
Subject: Coq: move function clause merging to keep measure argument intact

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

(limited to 'src')

diff --git a/src/rewrites.ml b/src/rewrites.ml
index afbba659..3cd89b89 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -5065,6 +5065,9 @@ let rewrite_defs_coq = [
   ("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);
   ("rewrite_explicit_measure", rewrite_explicit_measure);
   ("recheck_defs_without_effects", recheck_defs_without_effects);
   ("fix_val_specs", rewrite_fix_val_specs);
@@ -5074,7 +5077,6 @@ let rewrite_defs_coq = [
   ("internal_lets", rewrite_defs_internal_lets);
   ("remove_superfluous_letbinds", rewrite_defs_remove_superfluous_letbinds);
   ("remove_superfluous_returns", rewrite_defs_remove_superfluous_returns);
-  ("merge function clauses", merge_funcls);
   ("recheck_defs", recheck_defs)
   ]
 
-- 
cgit v1.2.3