diff options
Diffstat (limited to 'backend/Duplicateproof.v')
| -rw-r--r-- | backend/Duplicateproof.v | 5 |
1 files changed, 5 insertions, 0 deletions
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. |