aboutsummaryrefslogtreecommitdiff
path: root/src/AbstractInterpretation.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/AbstractInterpretation.v')
-rw-r--r--src/AbstractInterpretation.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/AbstractInterpretation.v b/src/AbstractInterpretation.v
index 463cc72cd..4d82b869a 100644
--- a/src/AbstractInterpretation.v
+++ b/src/AbstractInterpretation.v
@@ -377,6 +377,7 @@ Module Compilers.
| ident.Nat_mul as idc
| ident.Nat_add as idc
| ident.Nat_sub as idc
+ | ident.Nat_eqb as idc
| ident.List_seq as idc
=> fun x y => x <- x; y <- y; rSome (ident.interp idc x y)
| ident.List_repeat _