aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Reflection/TestCase.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v
index 5b56a5bee..31ca20fec 100644
--- a/src/Reflection/TestCase.v
+++ b/src/Reflection/TestCase.v
@@ -156,4 +156,4 @@ Definition example_expr_compiled
| None => True
end.
-Compute register_reassign Pos.eqb empty empty example_expr_compiled (Some 1%positive :: Some 2%positive :: None :: List.map Some (List.map Pos.of_nat (seq 3 20))).
+Compute register_reassign Pos.eqb empty empty example_expr_compiled (Some 1%positive :: Some 2%positive :: None :: List.map (@Some _) (List.map Pos.of_nat (seq 3 20))).