diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-15 17:48:30 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-15 17:48:30 -0400 |
commit | 30d8500955c86235a9270a9bf06e4a61fa28ef07 (patch) | |
tree | 5c0675cba67b57e9548ea0a9ff55293c14828170 /src/Arithmetic | |
parent | 139328c9e3efa8d22136c56e9a6a2cae176dfa9c (diff) |
Improve replace_match_with_destructuring_match
Now it handles matches under binders, e.g., under dlet. This fixes
https://github.com/mit-plv/fiat-crypto/issues/195#issuecomment-308724129.
Diffstat (limited to 'src/Arithmetic')
-rw-r--r-- | src/Arithmetic/Core.v | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index 7842c1b85..f0899c0e0 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -742,7 +742,7 @@ Module B. to_associational_cps p (fun P => Associational.mul_cps P [(1, x)] (fun R => from_associational_cps n R f)). - + (* This version of sub does not add balance; bounds must be carefully handled. *) Definition unbalanced_sub_cps {n} (p q: tuple Z n) @@ -1048,6 +1048,16 @@ Ltac replace_match_with_destructuring_match T := let v := replace_match_with_destructuring_match v in exact v) end) + | (fun a : ?A => @?f a) + => let T' := fresh in + let T' := fresh T' in + let T' := fresh T' in + constr:(fun a : A + => match f a with + | T' => ltac:(let v := (eval cbv beta delta [T'] in T') in + let v := replace_match_with_destructuring_match v in + exact v) + end) | ?x => x end. Ltac do_replace_match_with_destructuring_match_in_goal := |