diff options
| author | Brian Campbell | 2018-12-31 11:01:54 +0000 |
|---|---|---|
| committer | Brian Campbell | 2018-12-31 11:01:54 +0000 |
| commit | dccff374cc4ff0d2ac9737a1abd1907118af6456 (patch) | |
| tree | 5c264adb368663fa8affe9e0995fccfd352d55a1 /src | |
| parent | 269fdb0ed57814f3fbb41b206a67a3cc7bafc810 (diff) | |
Coq: move function clause merging to keep measure argument intact
Diffstat (limited to 'src')
| -rw-r--r-- | src/rewrites.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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) ] |