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/constrintern.ml | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3d484a02da..7bc4b81b20 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1219,6 +1219,11 @@ let alias_of als = match als.alias_ids with
 
 *)
 
+let is_zero s =
+  let rec aux i =
+    Int.equal (String.length s) i || (s.[i] == '0' && aux (i+1))
+  in aux 0
+
 let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2
 
 let product_of_cases_patterns aliases idspl =
@@ -1331,9 +1336,9 @@ let drop_notations_pattern looked_for genv =
         (* but not scopes in expl_pl *)
         let (argscs1,_) = find_remaining_scopes expl_pl pl g in
         CAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
-    | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral p) }],[]),[])
-	when Bigint.is_strictly_pos p ->
-      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes in
+    | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral (p,true)) }],[]),[])
+	when not (is_zero p) ->
+      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (p,false)) scopes in
       rcp_of_glob pat
     | CPatNotation ("( _ )",([a],[]),[]) ->
       in_pat top scopes a
@@ -1639,9 +1644,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	CAst.make ?loc @@
 	GLetIn (snd na, inc1, int,
           intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
-    | CNotation ("- _",([{ CAst.v = CPrim (Numeral p) }],[],[]))
-	when Bigint.is_strictly_pos p ->
-	intern env (CAst.make ?loc @@ CPrim (Numeral (Bigint.neg p)))
+    | CNotation ("- _",([{ CAst.v = CPrim (Numeral (p,true)) }],[],[]))
+         when not (is_zero p) ->
+       intern env (CAst.make ?loc @@ CPrim (Numeral (p,false)))
     | CNotation ("( _ )",([a],[],[])) -> intern env a
     | CNotation (ntn,args) ->
         intern_notation intern env ntnvars loc ntn args
-- 
cgit v1.2.3