Skip to content

Un-deprecating inspect, ctd. #2127

Closed
@jamesmckinna

Description

@jamesmckinna

Aaaargh! two/three bugs have crept into master after #1930, #2107:

  • README.Inspect no longer typechecks, because the import of PropositionalEquality fails to include the constructor name [_]; FIXED by [fixes #2127] Fixes #1930 import bug #2128
  • README no longer refers to README.Inspect, so the first bug goes un-noticed; PUSHED commit.
  • README.Inspect is marked as DEPRECATED; PUSHED commit.

The first should be fixed (my fault, I think, arising from #1930).
The second and third are, perhaps, moot, but should perhaps be reverted?

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions