coq-community/coq-tricks issues and pull requests

#38 - Fix the syntax explaining the warning attribute

Pull Request - State: closed - Opened by tchajed about 1 month ago

#38 - Fix the syntax explaining the warning attribute

Pull Request - State: closed - Opened by tchajed about 1 month ago

#37 - link to Function.v and mention Equations

Pull Request - State: closed - Opened by palmskog about 2 months ago - 2 comments

#37 - link to Function.v and mention Equations

Pull Request - State: closed - Opened by palmskog about 2 months ago - 2 comments

#36 - ensure all URLs have hyperlinks

Pull Request - State: closed - Opened by palmskog about 2 months ago

#36 - ensure all URLs have hyperlinks

Pull Request - State: closed - Opened by palmskog about 2 months ago

#35 - Deploy README.md to gh-pages branch as website

Pull Request - State: closed - Opened by palmskog about 2 months ago - 2 comments

#35 - Deploy README.md to gh-pages branch as website

Pull Request - State: closed - Opened by palmskog about 2 months ago - 2 comments

#34 - Add an explanation of skipping Qeds

Pull Request - State: closed - Opened by tchajed 2 months ago

#34 - Add an explanation of skipping Qeds

Pull Request - State: closed - Opened by tchajed 2 months ago

#33 - Reduce the preamble before the first trick

Pull Request - State: closed - Opened by tchajed 2 months ago

#33 - Reduce the preamble before the first trick

Pull Request - State: closed - Opened by tchajed 2 months ago

#32 - add meta.yml and generate boilerplate from templates

Pull Request - State: closed - Opened by palmskog 2 months ago - 3 comments

#32 - add meta.yml and generate boilerplate from templates

Pull Request - State: closed - Opened by palmskog 2 months ago - 3 comments

#31 - Automated deployment of web documentation

Issue - State: open - Opened by palmskog 2 months ago

#31 - Automated deployment of web documentation

Issue - State: open - Opened by palmskog 2 months ago

#30 - Fix use of CC0

Pull Request - State: closed - Opened by tchajed 2 months ago

#30 - Fix use of CC0

Pull Request - State: closed - Opened by tchajed 2 months ago

#29 - Update CI config

Pull Request - State: closed - Opened by tchajed 2 months ago

#29 - Update CI config

Pull Request - State: closed - Opened by tchajed 2 months ago

#28 - Add license

Pull Request - State: closed - Opened by tchajed 2 months ago

#28 - Add license

Pull Request - State: closed - Opened by tchajed 2 months ago

#27 - `Module A := A` vs `Include Module`

Issue - State: open - Opened by InfiniteEchoes 2 months ago

#27 - `Module A := A` vs `Include Module`

Issue - State: open - Opened by InfiniteEchoes 2 months ago

#26 - Clean up to various descriptions in README

Pull Request - State: closed - Opened by tchajed 2 months ago

#26 - Clean up to various descriptions in README

Pull Request - State: closed - Opened by tchajed 2 months ago

#25 - The uniform inheritance condition is gone

Pull Request - State: closed - Opened by tchajed 2 months ago

#25 - The uniform inheritance condition is gone

Pull Request - State: closed - Opened by tchajed 2 months ago

#24 - Add note about issue 9814

Pull Request - State: closed - Opened by tchajed 2 months ago

#24 - Add note about issue 9814

Pull Request - State: closed - Opened by tchajed 2 months ago

#23 - Add trick for defining Tactic Notations with multiple optional parameters

Pull Request - State: closed - Opened by snyke7 2 months ago - 1 comment

#23 - Add trick for defining Tactic Notations with multiple optional parameters

Pull Request - State: closed - Opened by snyke7 2 months ago - 1 comment

#22 - Add trick to avoid producing similar goals in case analyses.

Pull Request - State: closed - Opened by DasNaCl about 1 year ago - 1 comment

#22 - Add trick to avoid producing similar goals in case analyses.

Pull Request - State: closed - Opened by DasNaCl about 1 year ago - 1 comment

#21 - Add markdown-link-check to CI workflow

Pull Request - State: closed - Opened by tchajed over 1 year ago

#21 - Add markdown-link-check to CI workflow

Pull Request - State: closed - Opened by tchajed over 1 year ago

#20 - README.md: fix link to src/Bidirectional.v

Pull Request - State: closed - Opened by jdchristensen over 1 year ago - 1 comment

#20 - README.md: fix link to src/Bidirectional.v

Pull Request - State: closed - Opened by jdchristensen over 1 year ago - 1 comment

#19 - Typo in README, it should be `:= magic`

Pull Request - State: closed - Opened by yforster almost 2 years ago - 1 comment

#19 - Typo in README, it should be `:= magic`

Pull Request - State: closed - Opened by yforster almost 2 years ago - 1 comment

#18 - Trick suggestion

Issue - State: open - Opened by Yu-zh almost 4 years ago

#18 - Trick suggestion

Issue - State: open - Opened by Yu-zh almost 4 years ago

#17 - Trick suggestion: apply tactic to all subgoals

Issue - State: closed - Opened by ComFreek about 4 years ago - 2 comments

#17 - Trick suggestion: apply tactic to all subgoals

Issue - State: closed - Opened by ComFreek about 4 years ago - 2 comments

#16 - Inaccuracy in Search explanations

Issue - State: closed - Opened by Zimmi48 over 4 years ago - 1 comment

#16 - Inaccuracy in Search explanations

Issue - State: closed - Opened by Zimmi48 over 4 years ago - 1 comment

#15 - Check with named existentials

Pull Request - State: closed - Opened by ghost over 4 years ago - 1 comment

#15 - Check with named existentials

Pull Request - State: closed - Opened by ghost over 4 years ago - 1 comment

#14 - Make SmallInversions.v a bit shorter

Pull Request - State: closed - Opened by JasonGross about 5 years ago

#14 - Make SmallInversions.v a bit shorter

Pull Request - State: closed - Opened by JasonGross about 5 years ago

#13 - Gallina function application in Ltac

Issue - State: closed - Opened by cryslith over 5 years ago

#12 - convoy pattern

Issue - State: open - Opened by cryslith over 5 years ago

#11 - Give a minimal example of using sections with some of the tricks described

Issue - State: closed - Opened by tchajed almost 6 years ago

#10 - Mention small inversions

Issue - State: closed - Opened by JasonGross almost 6 years ago - 2 comments

#9 - Test against multiple Coq versions

Issue - State: open - Opened by tchajed almost 6 years ago - 1 comment

#8 - Build process is unnecessarily complicated

Issue - State: closed - Opened by tchajed almost 6 years ago - 1 comment

#7 - Integrate into the general coq-community ?

Issue - State: closed - Opened by spitters almost 6 years ago - 10 comments

#6 - Introduce categories for tricks?

Issue - State: closed - Opened by anton-trunov over 6 years ago - 3 comments

#5 - `dependent destruction` and `dependent induction` entry

Issue - State: closed - Opened by anton-trunov over 6 years ago - 1 comment

#4 - info_trivial has been fixed?

Issue - State: closed - Opened by anton-trunov almost 7 years ago - 1 comment

#3 - `Function` command for defining recursive functions.

Pull Request - State: closed - Opened by foreverbell almost 7 years ago - 4 comments

#2 - Explicit evars and strong induction cleanup

Pull Request - State: closed - Opened by anton-trunov about 7 years ago - 2 comments

#1 - Arguments

Issue - State: closed - Opened by JasonGross almost 8 years ago - 3 comments

GitHub / coq-community/coq-tricks issues and pull requests