From d038839a32978548051573286e22462d68d42ee6 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 26 Apr 2016 17:30:30 +0200
Subject: Constrexpr.Numeral stays uninterpreted (string+sign instead of
 BigInt.t)

 This string contains the base-10 representation of the number (big endian)

 Note that some inner parsing stuff still uses bigints, see egramcoq.ml
---
 interp/constrexpr_ops.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'interp/constrexpr_ops.ml')

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
 
-- 
cgit v1.2.3