diff options
| author | Maxime Dénès | 2017-06-15 22:00:17 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-15 22:00:17 +0200 |
| commit | 6467119bd15395bb5fae7d9c19dde17293842bd8 (patch) | |
| tree | 809a7156570542f796b4ed94d901a83468d78dc4 /interp/constrexpr_ops.ml | |
| parent | 9beec0fc6cc283294bbbda363a3f788ae56347d5 (diff) | |
| parent | 0b5ef21f936acbb89fa5b272efdcf3cf03de58cc (diff) | |
Merge PR#719: Constrexpr.Numeral without bigint
Diffstat (limited to 'interp/constrexpr_ops.ml')
| -rw-r--r-- | interp/constrexpr_ops.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 79e0e61646..396dde0465 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -45,8 +45,11 @@ let names_of_local_binders bl = (**********************************************************************) (* Functions on constr_expr *) +(* Note: redundant Numeral representations such as -0 and +0 (or different + numbers of leading zeros) are considered different here. *) + let prim_token_eq t1 t2 = match t1, t2 with -| Numeral i1, Numeral i2 -> Bigint.equal i1 i2 +| Numeral (n1,s1), Numeral (n2,s2) -> String.equal n1 n2 && s1 == s2 | String s1, String s2 -> String.equal s1 s2 | _ -> false |