Skip to content
Snippets Groups Projects

add make_simple_intropattern

Closed add make_simple_intropattern
ralf/make_simple_intropattern into master
Closed Ralf Jung requested to merge ralf/make_simple_intropattern into master

It's not needed for !512 (merged) after all, but could still be useful in the future.

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Robbert Krebbers
    Robbert Krebbers @robbertkrebbers
    Owner

    I am fine to include this, but I am also a bit hesitant of including a tactic that is not used. Would it make sense to add a test?

  • Ralf Jung
    Ralf Jung @jung
    Author Owner

    What the heck...

    Error: Ltac variable pat is bound to make_simple_intropattern [| n'] of type tacvalue which cannot be coerced to
an introduction pattern.

    How do I force evaluation? I've used this notation in !512 (merged) and it worked fine.^^

  • Ralf Jung
    Ralf Jung @jung
    Author Owner

    Or maybe Jason was right and tactic notations cannot return things, and my use in !512 (merged) wasn't actually valid. I didn't have a test checking that the collision avoidance actually worked.

  • Ralf Jung closed

    closed

Please register or sign in to reply