aboutsummaryrefslogtreecommitdiffstats
path: root/backend/Selectionproof.v
diff options
context:
space:
mode:
Diffstat (limited to 'backend/Selectionproof.v')
-rw-r--r--backend/Selectionproof.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index e94f85dd..c292b49c 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -26,9 +26,11 @@ Require Import Cminor.
Require Import Op.
Require Import CminorSel.
Require Import SelectOp.
+Require Import SelectDiv.
Require Import SelectLong.
Require Import Selection.
Require Import SelectOpproof.
+Require Import SelectDivproof.
Require Import SelectLongproof.
Open Local Scope cminorsel_scope.