diff options
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. |