diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-20 13:33:45 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-20 13:34:47 +0100 |
| commit | 85dc3bff6792d0cc2e1f7b3cc2446cd01428907b (patch) | |
| tree | 947efa7268d2cee5eec4c23e34075adb21e73c0e /backend/Selectionproof.v | |
| parent | 09faeee21a7d72eea8fc56f9ac505f01005d6cb5 (diff) | |
| download | compcert-kvx-85dc3bff6792d0cc2e1f7b3cc2446cd01428907b.tar.gz compcert-kvx-85dc3bff6792d0cc2e1f7b3cc2446cd01428907b.zip | |
Proof of div32/mod32/divf32/divf64 lemmas
Diffstat (limited to 'backend/Selectionproof.v')
| -rw-r--r-- | backend/Selectionproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
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. |