From 85dc3bff6792d0cc2e1f7b3cc2446cd01428907b Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 20 Mar 2019 13:33:45 +0100 Subject: Proof of div32/mod32/divf32/divf64 lemmas --- backend/Selectionproof.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'backend/Selectionproof.v') diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index dc01ad20..5a0fafaf 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -86,7 +86,7 @@ Lemma get_helpers_correct: forall p hf, get_helpers (prog_defmap p) = OK hf -> helper_functions_declared p hf. Proof. - intros. monadInv H. red; simpl. auto 20 using lookup_helper_correct. + intros. monadInv H. red; simpl. auto 22 using lookup_helper_correct. Qed. Theorem transf_program_match: @@ -106,7 +106,7 @@ Proof. { unfold helper_declared; intros. destruct (prog_defmap_linkorder _ _ _ _ H0 H1) as (gd & P & Q). inv Q. inv H3. auto. } - red in H. decompose [Logic.and] H; clear H. red; auto 20. + red in H. decompose [Logic.and] H; clear H. red; auto 22. Qed. (** * Correctness of the instruction selection functions for expressions *) @@ -164,7 +164,7 @@ Proof. generalize (match_program_defmap _ _ _ _ _ TRANSF id). unfold Cminor.fundef; rewrite H; intros R; inv R. inv H2. destruct H4 as (cu & A & B). monadInv B. auto. } - unfold helper_functions_declared; intros. decompose [Logic.and] H; clear H. auto 20. + unfold helper_functions_declared; intros. decompose [Logic.and] H; clear H. auto 22. Qed. Section CMCONSTR. -- cgit