aboutsummaryrefslogtreecommitdiff
path: root/src/AbstractInterpretation.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/AbstractInterpretation.v')
-rw-r--r--src/AbstractInterpretation.v5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/AbstractInterpretation.v b/src/AbstractInterpretation.v
index 808128025..ca0cb68bd 100644
--- a/src/AbstractInterpretation.v
+++ b/src/AbstractInterpretation.v
@@ -520,8 +520,8 @@ Module Compilers.
n
| None => ZRange.type.base.option.None
end
- | ident.eager_nat_rect_arrow _ _
| ident.nat_rect_arrow _ _
+ | ident.eager_nat_rect_arrow _ _
=> fun O_case S_case n v
=> match n with
| Some n
@@ -533,8 +533,8 @@ Module Compilers.
v
| None => ZRange.type.base.option.None
end
- | ident.eager_list_rect _ _
| ident.list_rect _ _
+ | ident.eager_list_rect _ _
=> fun N C ls
=> match ls with
| Some ls
@@ -545,6 +545,7 @@ Module Compilers.
ls
| None => ZRange.type.base.option.None
end
+ | ident.list_rect_arrow _ _ _
| ident.eager_list_rect_arrow _ _ _
=> fun N C ls v
=> match ls with