Merge PR#705: Fix bug #5019 (looping zify on dependent types)

2 files changed, 11 insertions, 1 deletions

diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 5f5f548f84..6c0e2d776d 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -174,12 +174,18 @@ Ltac zify_nat_op :=
      match isnat with
       | true => simpl (Z.of_nat (S a)) in H
       | _ => rewrite (Nat2Z.inj_succ a) in H
+      | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]),
+                hide [Z.of_nat (S a)] in this one hypothesis *)
+        change (Z.of_nat (S a)) with (Z_of_nat' (S a)) in H
      end
   | |- context [ Z.of_nat (S ?a) ] =>
      let isnat := isnatcst a in
      match isnat with
       | true => simpl (Z.of_nat (S a))
       | _ => rewrite (Nat2Z.inj_succ a)
+      | _ => (* if the [rewrite] fails (most likely a dependent occurence of [Z.of_nat (S a)]),
+                hide [Z.of_nat (S a)] in the goal *)
+        change (Z.of_nat (S a)) with (Z_of_nat' (S a))
      end
 
   (* atoms of type nat : we add a positivity condition (if not already there) *)
@@ -401,4 +407,3 @@ Ltac zify_N := repeat zify_N_rel; repeat zify_N_op; unfold Z_of_N' in *.
 (** The complete Z-ification tactic *)
 
 Ltac zify := repeat (zify_nat; zify_positive; zify_N); zify_op.
-
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.