diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/rewrites.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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); |