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/Constpropproof.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend/Constpropproof.v') diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index b14c4be0..e28519ca 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -493,7 +493,7 @@ Opaque builtin_strength_reduction. assert (C: cmatch (eval_condition cond rs ## args m) ac) by (eapply eval_static_condition_sound; eauto with va). rewrite H0 in C. - generalize (cond_strength_reduction_correct bc ae rs m EM cond args (aregs ae args) (refl_equal _)). + generalize (cond_strength_reduction_correct bc ae rs m EM cond args (aregs ae args) (eq_refl _)). destruct (cond_strength_reduction cond args (aregs ae args)) as [cond' args']. intros EV1 TCODE. left; exists O; exists (State s' (transf_function (romem_for cu) f) (Vptr sp0 Ptrofs.zero) (if b then ifso else ifnot) rs' m'); split. @@ -532,7 +532,7 @@ Opaque builtin_strength_reduction. destruct or; simpl; auto. - (* internal function *) - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [m2' [A B]]. simpl. unfold transf_function. left; exists O; econstructor; split. -- cgit