diff options
Diffstat (limited to 'backend/Duplicatepasses.v')
| -rw-r--r-- | backend/Duplicatepasses.v | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/backend/Duplicatepasses.v b/backend/Duplicatepasses.v index ffab2f59..7e58eedf 100644 --- a/backend/Duplicatepasses.v +++ b/backend/Duplicatepasses.v @@ -56,13 +56,3 @@ End LoopRotateOracle. Module Looprotateproof := DuplicateProof LoopRotateOracle. Module Looprotate := Looprotateproof. - -(** Lift If (TODO: this is a working title) *) - -Module LiftIfOracle <: DuplicateOracle. - Axiom duplicate_aux : function -> code * node * (PTree.t node). - Extract Constant duplicate_aux => "Duplicateaux.lift_if". -End LiftIfOracle. - -Module Liftifproof := DuplicateProof LiftIfOracle. -Module Liftif := Liftifproof. |