diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-12-04 16:40:51 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-12-04 16:40:51 -0500 |
| commit | 6b1851d4d349079cee43cfd4477e5f42c8fda37d (patch) | |
| tree | 2a851c47ecec0de188c373dd539e29f7f4dfe4e7 /src | |
| parent | 8742bd10f88593091dd45f99dd1b2358b8ac4000 (diff) | |
Yet more repeat fixing
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v index 7ac198a7e..0ea0503b1 100644 --- a/src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v +++ b/src/Experiments/NewPipeline/AbstractInterpretationZRangeProofs.v @@ -305,7 +305,7 @@ Module Compilers. | [ H : context[List.nth_error (List.rev _) _] |- _ ] => rewrite nth_error_rev in H | [ |- context[List.nth_error (List.rev _) _] ] => rewrite nth_error_rev | [ H : List.nth_error (Lists.List.repeat _ _) _ = Some _ |- _ ] => apply nth_error_repeat in H - | [ H : List.nth_error (repeat _ _) _ = Some _ |- _ ] => apply nth_error_repeat in H + | [ H : List.nth_error (List.repeat _ _) _ = Some _ |- _ ] => apply nth_error_repeat in H | [ H : length ?l1 = length ?l2 |- context[length ?l1] ] => rewrite H | [ H : length ?l1 = length ?l2, H' : context[length ?l1] |- _ ] => rewrite H in H' | [ |- context[List.flat_map _ _] ] => rewrite List.flat_map_concat_map, concat_fold_right_app |