From 8d5c6bb8f0cac1339dec7b730997ee30b1517073 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 22 Sep 2017 19:50:52 +0200 Subject: Remove coq warnings (#28) Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts. --- backend/Kildall.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/Kildall.v') diff --git a/backend/Kildall.v b/backend/Kildall.v index a2b49d56..8e712c05 100644 --- a/backend/Kildall.v +++ b/backend/Kildall.v @@ -1373,7 +1373,7 @@ Proof. replace (st1.(aval)!!pc) with res!!pc. fold l. destruct (basic_block_map s) eqn:BB. rewrite D. simpl. rewrite INV1. apply L.top_ge. auto. tauto. - elim (C H0 (refl_equal _)). intros X Y. rewrite Y. apply L.refl_ge. + elim (C H0 (eq_refl _)). intros X Y. rewrite Y. apply L.refl_ge. elim (U pc); intros E F. rewrite F. reflexivity. destruct (In_dec peq pc (successors instr)). right. eapply no_self_loop; eauto. -- cgit