diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-28 11:34:12 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-28 11:34:12 +0100 |
| commit | 2488c0eb8471eb07249a8b770c30c5cae2d629cc (patch) | |
| tree | 24646ad223b859225cef4bdb4b126c3caf609972 /backend/Duplicate.v | |
| parent | 04881502849e160dff04753bc8fa858b7967512c (diff) | |
| download | compcert-kvx-2488c0eb8471eb07249a8b770c30c5cae2d629cc.tar.gz compcert-kvx-2488c0eb8471eb07249a8b770c30c5cae2d629cc.zip | |
DuplicateParam -> DuplicateOracle + simpler Duplicatepasses
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. |