From 50ea7732118611a38e6aa6bced5c60dffb4eea3a Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Tue, 27 Oct 2020 12:07:49 +0100
Subject: Reworked Duplicate to be parametrized

---
 backend/Duplicateproof.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'backend/Duplicateproof.v')

diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index 62455076..719ff8e9 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -17,6 +17,9 @@ Require Import AST Linking Errors Globalenvs Smallstep.
 Require Import Coqlib Maps Events Values.
 Require Import Op RTL Duplicate.
 
+Module DuplicateProof (D: DuplicateParam).
+Include Duplicate D.
+
 Local Open Scope positive_scope.
 
 (** * Definition of [match_states] (independently of the translation) *)
@@ -535,3 +538,5 @@ Proof.
 Qed.
 
 End PRESERVATION.
+
+End DuplicateProof.
-- 
cgit