Skip to content

Commit 4ab4c5c

Browse files
committed
Qualify stdlib import
1 parent 859d59b commit 4ab4c5c

1 file changed

Lines changed: 4 additions & 12 deletions

File tree

backend/CminorSel.v

Lines changed: 4 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -12,18 +12,10 @@
1212

1313
(** The Cminor language after instruction selection. *)
1414

15-
Require Import Recdef.
16-
Require Import Coqlib.
17-
Require Import Maps.
18-
Require Import AST.
19-
Require Import Integers.
20-
Require Import Events.
21-
Require Import Values.
22-
Require Import Memory.
23-
Require Import Cminor.
24-
Require Import Op.
25-
Require Import Globalenvs.
26-
Require Import Smallstep.
15+
From Coq Require Import Recdef.
16+
Require Import Coqlib Maps AST Integers Events Values Memory.
17+
Require Import Cminor Op.
18+
Require Import Globalenvs Smallstep.
2719

2820
(** * Abstract syntax *)
2921

0 commit comments

Comments
 (0)