diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-11-14 23:03:30 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-11-14 23:03:30 +0100 |
| commit | 009d577cc3f590d525146a1afb87aa8e6d6a4b59 (patch) | |
| tree | 9bdb68243e74bca24ea3cf942549e0c3bb6c8ad8 /backend | |
| parent | 2e7ec13820d0df8bb9e61f911ed2cd3271d6fed4 (diff) | |
| download | compcert-kvx-009d577cc3f590d525146a1afb87aa8e6d6a4b59.tar.gz compcert-kvx-009d577cc3f590d525146a1afb87aa8e6d6a4b59.zip | |
merge merge merge
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Lineartyping.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index d0971dbd..0e3b7c8e 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -325,7 +325,7 @@ Local Opaque mreg_type. 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. - (* apply wt_undef_regs; auto. *) + apply wt_undef_regs; auto. - (* load *) simpl in *; InvBooleans. econstructor; eauto. |