diff options
| author | Maxime Dénès <mail@maximedenes.fr> | 2016-09-21 13:40:26 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-01-09 14:58:03 +0100 |
| commit | e61eb63a62560929b6b9856b29ba8557ab8dc53d (patch) | |
| tree | 656d3317141e683c44f3dfa2276cfe4a30b4bd0c /cfrontend/Ctypes.v | |
| parent | 747ad5bd8c364684256fc7dd306cd475401fe1b0 (diff) | |
| download | compcert-kvx-e61eb63a62560929b6b9856b29ba8557ab8dc53d.tar.gz compcert-kvx-e61eb63a62560929b6b9856b29ba8557ab8dc53d.zip | |
The subst tactic has become more powerful.
Diffstat (limited to 'cfrontend/Ctypes.v')
| -rw-r--r-- | cfrontend/Ctypes.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 0794743d..7b689674 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -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. |