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/Duplicateproof.v | |
| parent | 04881502849e160dff04753bc8fa858b7967512c (diff) | |
| download | compcert-kvx-2488c0eb8471eb07249a8b770c30c5cae2d629cc.tar.gz compcert-kvx-2488c0eb8471eb07249a8b770c30c5cae2d629cc.zip | |
DuplicateParam -> DuplicateOracle + simpler Duplicatepasses
Diffstat (limited to 'backend/Duplicateproof.v')
| -rw-r--r-- | backend/Duplicateproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 719ff8e9..2480ccf0 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -17,7 +17,7 @@ Require Import AST Linking Errors Globalenvs Smallstep. Require Import Coqlib Maps Events Values. Require Import Op RTL Duplicate. -Module DuplicateProof (D: DuplicateParam). +Module DuplicateProof (D: DuplicateOracle). Include Duplicate D. Local Open Scope positive_scope. |