From e61eb63a62560929b6b9856b29ba8557ab8dc53d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 21 Sep 2016 13:40:26 +0200 Subject: The subst tactic has become more powerful. --- cfrontend/Ctypes.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cfrontend') 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. -- cgit From 5e2454ecba7c99e4615f123d71a227fddbca3908 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 21 Sep 2016 13:43:21 +0200 Subject: An hypothesis has changed name. Not sure why, but it would be safer not to rely on automatic naming. --- cfrontend/Ctypes.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cfrontend') diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 7b689674..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. -- cgit From 88bf09d3673dbda96c216a3e037d503a9664795e Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 21 Dec 2016 01:22:46 +0100 Subject: Some backward compatible Ltac fixes, necessary for 8.6. --- cfrontend/Cexec.v | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 4dcf2a47..a9ffcd3d 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -130,8 +130,8 @@ Definition val_of_eventval (ev: eventval) (t: typ) : option val := Ltac mydestr := match goal with - | [ |- None = Some _ -> _ ] => intro X; discriminate - | [ |- Some _ = Some _ -> _ ] => intro X; inv X + | [ |- None = Some _ -> _ ] => let X := fresh "X" in intro X; discriminate + | [ |- Some _ = Some _ -> _ ] => let X := fresh "X" in intro X; inv X | [ |- match ?x with Some _ => _ | None => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr | [ |- match ?x with true => _ | false => _ end = Some _ -> _ ] => destruct x eqn:?; mydestr | [ |- match ?x with left _ => _ | right _ => _ end = Some _ -> _ ] => destruct x; mydestr @@ -2038,12 +2038,14 @@ Definition do_step (w: world) (s: state) : list transition := Ltac myinv := match goal with - | [ |- In _ nil -> _ ] => intro X; elim X + | [ |- In _ nil -> _ ] => let X := fresh "X" in intro X; elim X | [ |- In _ (ret _ _) -> _ ] => + let X := fresh "X" in intro X; elim X; clear X; - [intro EQ; unfold ret in EQ; inv EQ; myinv | myinv] + [let EQ := fresh "EQ" in intro EQ; unfold ret in EQ; inv EQ; myinv | myinv] | [ |- In _ (_ :: nil) -> _ ] => - intro X; elim X; clear X; [intro EQ; inv EQ; myinv | myinv] + let X := fresh "X" in + intro X; elim X; clear X; [let EQ := fresh "EQ" in intro EQ; inv EQ; myinv | myinv] | [ |- In _ (match ?x with Some _ => _ | None => _ end) -> _ ] => destruct x eqn:?; myinv | [ |- In _ (match ?x with false => _ | true => _ end) -> _ ] => destruct x eqn:?; myinv | [ |- In _ (match ?x with left _ => _ | right _ => _ end) -> _ ] => destruct x; myinv -- cgit