move `Require Import` to top of the file #1334

Closed

Milestone

opened

analysis/theories/sequences.v

Line 116 in bab1cb0

From mathcomp Require Import mathcomp_extra.

Metadata

Assignees

No one assigned

Labels

No labels

No labels

Type

No type

Projects

No projects

Milestone

1.5.0

Relationships

None yet

Development

No branches or pull requests