From 2488c0eb8471eb07249a8b770c30c5cae2d629cc Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Wed, 28 Oct 2020 11:34:12 +0100
Subject: DuplicateParam -> DuplicateOracle + simpler Duplicatepasses

---
 backend/Duplicateproof.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backend/Duplicateproof.v')

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.
-- 
cgit