diff options
| -rw-r--r-- | plugins/omega/PreOmega.v | 7 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5019.v (renamed from test-suite/bugs/opened/5019.v) | 3 |
2 files changed, 8 insertions, 2 deletions
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v index 5f5f548f8..6c0e2d776 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/opened/5019.v b/test-suite/bugs/closed/5019.v index 09622097c..7c973f88b 100644 --- a/test-suite/bugs/opened/5019.v +++ b/test-suite/bugs/closed/5019.v @@ -1,4 +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. - Fail Timeout 1 zify. + Timeout 1 zify. (* used to loop forever; should take < 0.01 s *) +Admitted. |