coq-community/coq-tricks

Issues

• Automated deployment of web documentation

  #31 opened 6 months ago by palmskog
  0

• Integrate into the general coq-community ?

  #7 opened 6 months ago by spitters
  10

• `Module A := A` vs `Include Module`

  #27 opened 6 months ago by InfiniteEchoes
  0

• Trick suggestion

  #18 opened 4 years ago by Yu-zh
  0

• Trick suggestion: apply tactic to all subgoals

  #17 opened 4 years ago by ComFreek
  2

• Inaccuracy in Search explanations

  #16 opened 5 years ago by Zimmi48
  1

• Test against multiple Coq versions

  #9 opened 6 years ago by tchajed
  1

• Gallina function application in Ltac

  #13 opened 5 years ago by cryslith
  0

• Mention small inversions

  #10 opened 6 years ago by JasonGross
  2

• convoy pattern

  #12 opened 6 years ago by cryslith
  0

• Give a minimal example of using sections with some of the tricks described

  #11 opened 6 years ago by tchajed
  0

• Build process is unnecessarily complicated

  #8 opened 6 years ago by tchajed
  1

• Introduce categories for tricks?

  #6 opened 7 years ago by anton-trunov
  3

• `dependent destruction` and `dependent induction` entry

  #5 opened 7 years ago by anton-trunov
  1

• info_trivial has been fixed?

  #4 opened 7 years ago by anton-trunov
  1

• Arguments

  #1 opened 8 years ago by JasonGross
  3