diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-11-14 22:50:45 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-11-14 22:50:45 +0100 |
| commit | 2e7ec13820d0df8bb9e61f911ed2cd3271d6fed4 (patch) | |
| tree | 6d8a54deb9b45a3484d63c312187d2d89d18491d /backend | |
| parent | cee223374ba6a1e0c8f2461536c16e9cf603dfa5 (diff) | |
| parent | 01b5b9878476d01fbe8d7cdaecc0e5f1e0395544 (diff) | |
| download | compcert-kvx-2e7ec13820d0df8bb9e61f911ed2cd3271d6fed4.tar.gz compcert-kvx-2e7ec13820d0df8bb9e61f911ed2cd3271d6fed4.zip | |
Merge branch 'mppa-work-upstream-merge' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work-upstream-merge
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Lineartyping.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 0fa6838c..d0971dbd 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -321,9 +321,7 @@ Local Opaque mreg_type. + (* other ops *) destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans. econstructor; eauto. - - apply wt_setreg; auto; try (apply wt_undef_regs; auto). - eapply Val.has_subtype; eauto. + apply wt_setreg. eapply Val.has_subtype; eauto. change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto. red; intros; subst op. simpl in ISMOVE. destruct args; try discriminate. destruct args; discriminate. |