aboutsummaryrefslogtreecommitdiff
path: root/src/AbstractInterpretationWf.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/AbstractInterpretationWf.v')
-rw-r--r--src/AbstractInterpretationWf.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/AbstractInterpretationWf.v b/src/AbstractInterpretationWf.v
index a1e2f180e..85eef1cae 100644
--- a/src/AbstractInterpretationWf.v
+++ b/src/AbstractInterpretationWf.v
@@ -699,6 +699,7 @@ Module Compilers.
| solve [ eauto ]
| apply NatUtil.nat_rect_Proper_nondep
| apply ListUtil.list_rect_Proper
+ | apply ListUtil.list_rect_arrow_Proper
| apply ListUtil.list_case_Proper
| apply ListUtil.pointwise_map
| apply ListUtil.fold_right_Proper