Skip to content

EclecticLib.v --> Tactic failure: resersible in 1st order mode  #135

@nanoeng

Description

@nanoeng

Howdy,

Every time I try to compile the current EclecticLib.v using the CoqIDE compiler, the following error messages show up

  • 795: Tactic failure: reversible in 1st order mode.
  • 800: Tactic failure: reversible in 1st order mode.
  • 893: [Focus] Wrong bullet +: Current bullet + is not finished.
  • 904: The reference h was not found in the current environment.

Would appreciate it if you guys could please let me know if I'm missing anything.

Thanks in advance!

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No 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