aboutsummaryrefslogtreecommitdiff
path: root/src/CompilersTestCases.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/CompilersTestCases.v')
-rw-r--r--src/CompilersTestCases.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/CompilersTestCases.v b/src/CompilersTestCases.v
index c02b4e2fc..d5c8b2579 100644
--- a/src/CompilersTestCases.v
+++ b/src/CompilersTestCases.v
@@ -61,7 +61,7 @@ Module testrewrite.
(RewriteRules.RewriteNBE (fun var =>
(\z , ((\ x , expr_let y := ##5 in $y + ($z + (#ident.fst @ $x + #ident.snd @ $x)))
@ (##1, ##7)))%expr) _)
- (Some r[0~>100]%zrange, tt).
+ (Datatypes.Some r[0~>100]%zrange, tt).
End testrewrite.
Module testpartial.
Import expr.
@@ -85,7 +85,7 @@ Module testpartial.
partial.default_relax_zrange
(\z , ((\ x , expr_let y := ##5 in $y + ($z + (#ident.fst @ $x + #ident.snd @ $x)))
@ (##1, ##7)))%expr
- (Some r[0~>100]%zrange, tt).
+ (Datatypes.Some r[0~>100]%zrange, tt).
End testpartial.
Module test2.