aboutsummaryrefslogtreecommitdiff
path: root/src/Language.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Language.v')
-rw-r--r--src/Language.v2
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