diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-13 09:57:27 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-02-13 09:57:27 +0100 |
| commit | 9ceacf45af6bfe396e36938e2573348ac4d07603 (patch) | |
| tree | bb5200ab8fa1ab24ad547a10e5626585f307c6bf /cfrontend/Ctypes.v | |
| parent | 236d8a48288ea5845466408cf9d0be2ccd68f9a8 (diff) | |
| parent | c514b1e62302bb674075cd32a412ed47a57cbb5b (diff) | |
| download | compcert-9ceacf45af6bfe396e36938e2573348ac4d07603.tar.gz compcert-9ceacf45af6bfe396e36938e2573348ac4d07603.zip | |
Merge branch 'coq-8.6' of https://github.com/maximedenes/CompCert into maximedenes-coq-8.6
Diffstat (limited to 'cfrontend/Ctypes.v')
| -rw-r--r-- | cfrontend/Ctypes.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 0794743d..8d6cdb24 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -1064,7 +1064,7 @@ Proof. destruct (complete_members env m) eqn:C; simplify_eq EQ. clear EQ; intros EQ. rewrite PTree.gsspec. intros [A|A]; auto. destruct (peq id id0); auto. - inv A. rewrite <- H1; auto. + inv A. rewrite <- H0; auto. } intros. exploit REC; eauto. rewrite PTree.gempty. intuition congruence. Qed. @@ -1519,7 +1519,7 @@ Local Transparent Linker_program. - intros. exploit link_match_fundef; eauto. intros (tf & A & B). exists tf; auto. - intros. Local Transparent Linker_types. - simpl in *. destruct (type_eq v1 v2); inv H4. subst v tv2. exists tv1; rewrite dec_eq_true; auto. + simpl in *. destruct (type_eq v1 v2); inv H4. exists v; rewrite dec_eq_true; auto. - eauto. - eauto. - eauto. |