aboutsummaryrefslogtreecommitdiff
path: root/src/Language.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Language.v')
-rw-r--r--src/Language.v4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Language.v b/src/Language.v
index 74c34b2f2..703449eca 100644
--- a/src/Language.v
+++ b/src/Language.v
@@ -1405,6 +1405,10 @@ Module Compilers.
| @List.app ?A
=> let rA := base.reify A in
then_tac (@ident.List_app rA)
+ | @List.map ?A ?B
+ => let rA := base.reify A in
+ let rB := base.reify B in
+ then_tac (@ident.List_map rA rB)
| @List.rev ?A
=> let rA := base.reify A in
then_tac (@ident.List_rev rA)