Skip to content

coqdoc formatting command #1071

@affeldt-aist

Description

@affeldt-aist

(** begin hide *)
(* Hint View for move / Inversible.sort inv | 2. *)
(* Hint View for apply / Inversible.sort inv | 2. *)
(** end hide *)

do we have a policy for the use of begin hide from coqdoc or can this be removed?

Metadata

Metadata

Assignees

No one assigned

    Labels

    question ❓There is an unanswered question here

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions