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/Allocproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/Allocproof.v') diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 6c10d27f..4b75e34d 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -2444,7 +2444,7 @@ Proof. (* internal function *) - monadInv FUN. simpl in *. destruct (transf_function_inv _ _ EQ). - exploit Mem.alloc_extends; eauto. apply Zle_refl. rewrite H8; apply Zle_refl. + exploit Mem.alloc_extends; eauto. apply Z.le_refl. rewrite H8; apply Z.le_refl. intros [m'' [U V]]. assert (WTRS: wt_regset env (init_regs args (fn_params f))). { apply wt_init_regs. inv H0. rewrite wt_params. rewrite H9. auto. } -- cgit