Skip to content

Reduce the number of From mathcomp Require Import #1875

@affeldt-aist

Description

@affeldt-aist

What about writing:

From mathcomp Require Import blah0 blah1 blah2.

instead of

From mathcomp Require Import blah0.
From mathcomp Require Import blah1.
From mathcomp Require Import blah2.

?
We could spare a few lines while keeping the 80 characters width constraint.
Maybe there is a technical reason?

Metadata

Metadata

Assignees

No one assigned

    Labels

    question ❓There is an unanswered question here

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions