Skip to content

Use #[export] instead of #[global]? #221

@Lysxia

Description

@Lysxia

This migration is a bit painful because we also have to figure out what modules should reexport what other modules.

Metadata

Metadata

Assignees

No one assigned

    Labels

    coq-devQuestions related to best practices for Coq programmingquestionFurther information is requested

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions