From 4af77d01c434ff11f0899d504628f4ff91c49142 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 30 May 2017 12:11:28 -0400
Subject: Add opened bug 5019

---
 test-suite/bugs/opened/5019.v | 4 ++++
 1 file changed, 4 insertions(+)
 create mode 100644 test-suite/bugs/opened/5019.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/opened/5019.v b/test-suite/bugs/opened/5019.v
new file mode 100644
index 0000000000..09622097c5
--- /dev/null
+++ b/test-suite/bugs/opened/5019.v
@@ -0,0 +1,4 @@
+Require Import Coq.ZArith.ZArith.
+Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d.
+  clear; intros.
+  Fail Timeout 1 zify.
-- 
cgit v1.2.3


From 1d6a1036a7c472e1f20c5ec586d2484203a2fe2e Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 30 May 2017 12:48:47 -0400
Subject: Fix bug #5019 (looping zify on dependent types)

This fixes [bug #5019](https://coq.inria.fr/bugs/show_bug.cgi?id=5019),
"[zify] loops on dependent types"; before, we would see a `Z.of_nat (S
?k)` which could not be turned into `Z.succ (Z.of_nat k)`, add a
hypothesis of the shape `0 <= Z.of_nat (S k)`, turn that into a
hypothesis of the shape `0 <= Z.succ (Z.of_nat k)`, and loop forever on
this.

This may not be the "right" fix (there may be cases where `zify` should
succeed where it still fails with this change), but this is a pure
bugfix in the sense that the only places where it changes the behavior
of `zify` are the places where, previously, `zify` looped forever.
---
 test-suite/bugs/closed/5019.v | 5 +++++
 test-suite/bugs/opened/5019.v | 4 ----
 2 files changed, 5 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/bugs/closed/5019.v
 delete mode 100644 test-suite/bugs/opened/5019.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5019.v b/test-suite/bugs/closed/5019.v
new file mode 100644
index 0000000000..7c973f88b5
--- /dev/null
+++ b/test-suite/bugs/closed/5019.v
@@ -0,0 +1,5 @@
+Require Import Coq.ZArith.ZArith.
+Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d.
+  clear; intros.
+  Timeout 1 zify. (* used to loop forever; should take < 0.01 s *)
+Admitted.
diff --git a/test-suite/bugs/opened/5019.v b/test-suite/bugs/opened/5019.v
deleted file mode 100644
index 09622097c5..0000000000
--- a/test-suite/bugs/opened/5019.v
+++ /dev/null
@@ -1,4 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Goal forall (T0 : Z -> Type) (k : nat) d (P : T0 (Z.of_nat (S k)) -> Prop), P d.
-  clear; intros.
-  Fail Timeout 1 zify.
-- 
cgit v1.2.3