diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-01-23 17:12:48 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-01-23 17:12:48 +0100 |
| commit | 903ed0cfa5cb91d99ee373fc8cf408c0a80f968a (patch) | |
| tree | aa2c764c4269a42e4a947182f1a76c3585cc15d3 /backend/Duplicateproof.v | |
| parent | 1acafe8f7f61a8908f47de4c98f3d873f8f9afbd (diff) | |
| download | compcert-kvx-903ed0cfa5cb91d99ee373fc8cf408c0a80f968a.tar.gz compcert-kvx-903ed0cfa5cb91d99ee373fc8cf408c0a80f968a.zip | |
Revert "Modified the hook for the oracle"
This reverts commit 04a46f516487557df00f43453c8decbc8567c458.
It was actually not needed
Diffstat (limited to 'backend/Duplicateproof.v')
| -rw-r--r-- | backend/Duplicateproof.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index c285e4b3..a8e9b16b 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -79,8 +79,7 @@ Theorem transf_function_preserves: transf_function f = OK f' -> fn_sig f = fn_sig f' /\ fn_params f = fn_params f' /\ fn_stacksize f = fn_stacksize f'. Proof. - intros. unfold transf_function in H. destruct (duplicate_aux _) as (tctemp & invl). destruct tctemp as (tcte & mp). destruct tcte as (tc & te). - monadInv H. + intros. unfold transf_function in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). monadInv H. repeat (split; try reflexivity). Qed. @@ -235,7 +234,7 @@ Theorem transf_function_correct f f': Proof. unfold transf_function. intros TRANSF. - destruct (duplicate_aux _) as (tctemp & invl). destruct tctemp as (tcte & mp). destruct tcte as (tc & te). + destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). monadInv TRANSF. unfold verify_mapping in EQ. monadInv EQ. exists mp; constructor 1; simpl; auto. |