Support Nat.eqb in reification

1 files changed, 2 insertions, 0 deletions

diff --git a/src/Language.v b/src/Language.v
index eba5cf85a..e4c5057db 100644
--- a/src/Language.v
+++ b/src/Language.v
@@ -855,6 +855,7 @@ Module Compilers.
         | Nat_mul : ident (nat -> nat -> nat)
         | Nat_add : ident (nat -> nat -> nat)
         | Nat_sub : ident (nat -> nat -> nat)
+        | Nat_eqb : ident (nat -> nat -> bool)
         | nil {t} : ident (list t)
         | cons {t:base.type} : ident (t -> list t -> list t)
         | pair {A B:base.type} : ident (A -> B -> A * B)
@@ -995,6 +996,7 @@ Module Compilers.
              | Nat_mul => Nat.mul
              | Nat_add => Nat.add
              | Nat_sub => Nat.sub
+             | Nat_eqb => Nat.eqb
              | nil t => Datatypes.nil
              | cons t => Datatypes.cons
              | pair A B => Datatypes.pair