aboutsummaryrefslogtreecommitdiff
path: root/src/Language.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-01-25 16:49:21 -0500
committerGravatar Jason Gross <jgross@mit.edu>2019-01-25 16:49:21 -0500
commit6b06c0befa56137d479985a4c3912a75f3858cc3 (patch)
tree6c19ec96543d6db6a7021ba94ceda03b4a947fa4 /src/Language.v
parenta714d4b1cc90089b80ac475f5b6882f05e98c355 (diff)
Actually support Nat.eqb in reification
Diffstat (limited to 'src/Language.v')
-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