aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Language.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Language.v b/src/Language.v
index e4c5057db..6eac36949 100644
--- a/src/Language.v
+++ b/src/Language.v
@@ -1143,6 +1143,7 @@ Module Compilers.
| Nat.succ => then_tac Nat_succ
| Nat.add => then_tac Nat_add
| Nat.sub => then_tac Nat_sub
+ | Nat.eqb => then_tac Nat_eqb
| Nat.mul => then_tac Nat_mul
| Nat.max => then_tac Nat_max
| Nat.pred => then_tac Nat_pred