From 903ed0cfa5cb91d99ee373fc8cf408c0a80f968a Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 23 Jan 2020 17:12:48 +0100 Subject: Revert "Modified the hook for the oracle" This reverts commit 04a46f516487557df00f43453c8decbc8567c458. It was actually not needed --- backend/Duplicateproof.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'backend/Duplicateproof.v') 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. -- cgit