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
---
 test-suite/bugs/closed/3036.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3036.v b/test-suite/bugs/closed/3036.v
index 451bec9b20..3b57310d6e 100644
--- a/test-suite/bugs/closed/3036.v
+++ b/test-suite/bugs/closed/3036.v
@@ -15,11 +15,11 @@ Definition perm := Qc.
 Locate Qle_bool.
 
 Definition compatibleb (p1 p2 : perm) : bool :=
-let p1pos := Qle_bool 00 p1 in
-  let p2pos := Qle_bool 00 p2 in
+let p1pos := Qle_bool 0 p1 in
+  let p2pos := Qle_bool 0 p2 in
     negb (
          (p1pos && p2pos)
-      || ((p1pos || p2pos) && (negb (Qle_bool 00 ((p1 + p2)%Qc)))))%Qc.
+      || ((p1pos || p2pos) && (negb (Qle_bool 0 ((p1 + p2)%Qc)))))%Qc.
 
 Definition compatible (p1 p2 : perm) := compatibleb p1 p2 = true.
 
-- 
cgit v1.2.3