diff options
| -rw-r--r-- | backend/Deadcodeproof.v | 8 | ||||
| -rw-r--r-- | cfrontend/Cexec.v | 13 | ||||
| -rw-r--r-- | cparser/validator/Interpreter_complete.v | 1 |
3 files changed, 13 insertions, 9 deletions
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index a8d79c3f..5c293ee1 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -717,8 +717,8 @@ Ltac TransfInstr := FUN: transf_function _ _ = OK _, ANL: analyze _ _ = Some _ |- _ ] => generalize (transf_function_at _ _ _ _ _ _ FUN ANL INSTR); - intro TI; - unfold transf_instr in TI + let TI := fresh "TI" in + intro TI; unfold transf_instr in TI end. Ltac UseTransfer := @@ -1026,7 +1026,7 @@ Ltac UseTransfer := exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D). exploit external_call_mem_extends; eauto 2 with na. eapply magree_extends; eauto. intros. apply nlive_all. - intros (v' & tm' & P & Q & R & S & T). + intros (v' & tm' & P & Q & R & S). econstructor; split. eapply exec_Ibuiltin; eauto. apply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. @@ -1077,7 +1077,7 @@ Ltac UseTransfer := - (* external function *) exploit external_call_mem_extends; eauto. - intros (res' & tm' & A & B & C & D & E). + intros (res' & tm' & A & B & C & D). simpl in FUN. inv FUN. econstructor; split. econstructor; eauto. diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index b7329a4d..a2bfa6e1 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -218,8 +218,8 @@ Definition do_volatile_store (w: world) (chunk: memory_chunk) (m: mem) (b: block 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 @@ -2034,12 +2034,15 @@ 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 diff --git a/cparser/validator/Interpreter_complete.v b/cparser/validator/Interpreter_complete.v index eb407061..ff88571b 100644 --- a/cparser/validator/Interpreter_complete.v +++ b/cparser/validator/Interpreter_complete.v @@ -14,6 +14,7 @@ (* *********************************************************************) Require Import Streams. +Require Import ProofIrrelevance. Require Import Equality. Require Import List. Require Import Syntax. |