Revert "Modified the hook for the oracle"

This reverts commit 04a46f516487557df00f43453c8decbc8567c458.

It was actually not needed

1 files changed, 5 insertions, 8 deletions

diff --git a/backend/Duplicate.v b/backend/Duplicate.v
index 18869f39..82c17367 100644
--- a/backend/Duplicate.v
+++ b/backend/Duplicate.v
@@ -1,6 +1,5 @@
 (** RTL node duplication using external oracle. Used to form superblock
-  structures. Also swaps the ifso and ifnot of the Icond based on the
-  traces identified by the oracle *)
+  structures *)
 
 Require Import AST RTL Maps Globalenvs.
 Require Import Coqlib Errors Op.
@@ -8,10 +7,9 @@ Require Import Coqlib Errors Op.
 Local Open Scope error_monad_scope.
 Local Open Scope positive_scope.
 
-(** External oracle returning the new RTL code,
-    along with the new entrypoint, a mapping of new nodes to old nodes,
-    and a list of nodes to invert the condition on *)
-Axiom duplicate_aux: function -> code * node * (PTree.t node) * (list node).
+(** External oracle returning the new RTL code (entry point unchanged),
+    along with the new entrypoint, and a mapping of new nodes to old nodes *)
+Axiom duplicate_aux: function -> code * node * (PTree.t node).
 
 Extract Constant duplicate_aux => "Duplicateaux.duplicate_aux".
 
@@ -192,8 +190,7 @@ Definition verify_mapping dupmap (f f': function) : res unit :=
 (** * Entry points *)
 
 Definition transf_function (f: function) : res function :=
-  let (tctedupmap, invertlist) := duplicate_aux f in
-  let (tcte, dupmap) := tctedupmap in
+  let (tcte, dupmap) := duplicate_aux f in
   let (tc, te) := tcte in
   let f' := mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in
   do u <- verify_mapping dupmap f f';