diff options
Diffstat (limited to 'backend/Duplicate.v')
-rw-r--r-- | backend/Duplicate.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 6ae5475d..7dea752b 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -20,17 +20,17 @@ Require Import Coqlib Errors Op. -Module Type DuplicateParam. +Module Type DuplicateOracle. (** External oracle returning the new RTL code (entry point unchanged), along with the new entrypoint, and a mapping of new nodes to old nodes *) Parameter duplicate_aux: function -> code * node * (PTree.t node). -End DuplicateParam. +End DuplicateOracle. -Module Duplicate (D: DuplicateParam). +Module Duplicate (D: DuplicateOracle). Export D. |