Skip to content

Tactic serialization of "pending" generates tactic that doesn't parse due to string escaping #79

@rbohrer

Description

@rbohrer

Self-explanatory but sad. I believe this bug goes back to at least the introduction of tactic annotations.

But it came up again because some of my proofs started pending if I export them and reimport them.

Metadata

Metadata

Assignees

No one assigned

    Labels

    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