issues
search
impermeable
/
coq-waterproof
The Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to prove mathematical statements.
https://impermeable.github.io/
GNU Lesser General Public License v3.0
30
stars
9
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Adapt to coq/coq#19690 (Hint Extern respects default proof mode)
#85
SkySkimmer
opened
4 days ago
0
Allow for standard math notation in quantifiers
#84
jim-portegies
closed
2 days ago
2
Adapt to coq/coq#19620 (Global.push_context_set no strict argument)
#83
SkySkimmer
closed
5 days ago
1
Fix lsp version, add VSCode plugin instructions
#82
pimotte
closed
3 weeks ago
0
Feat obtain multiple vars + warn on unexpected variable names.
#81
jim-portegies
closed
3 weeks ago
2
Feat test warnings and errors
#80
jim-portegies
closed
3 weeks ago
0
Adapt to https://github.com/coq/coq/pull/19530
#79
proux01
opened
1 month ago
0
Update README and introduce Developer instructions
#78
jim-portegies
closed
1 month ago
0
fix: build of the documentation
#77
jim-portegies
closed
1 month ago
0
Bring the newest features from main into coq-master
#76
jim-portegies
closed
1 month ago
1
Simplify build process
#75
jim-portegies
closed
1 month ago
0
Create a devcontainer for the project
#74
jim-portegies
closed
1 month ago
0
Refactor ffi again
#73
jim-portegies
closed
1 month ago
1
Refactor ffi & simplify build process
#72
jim-portegies
closed
1 month ago
1
Feat binders
#71
jim-portegies
closed
1 month ago
1
Specialize blank
#70
jim-portegies
closed
1 month ago
0
feat: Provide suggestions to users on how to use forall- and exists-statements.
#69
jellooo038
closed
1 month ago
2
feat: Tactics for postponing proof of statement.
#68
jellooo038
closed
1 month ago
1
fix: Throw fake syntax error if user-input is read as e.g. "Obtain such a Qed."
#67
jellooo038
closed
1 month ago
0
feat: 'Expand definition' tactic unfolds definition in all statements
#66
jellooo038
closed
1 month ago
1
Merge 8.17 into main (allows for choosing blanks)
#65
jim-portegies
closed
2 months ago
0
Renamed variables to prevent having actual exercise solution in repo
#64
jellooo038
closed
2 months ago
0
Fix application of explicit coercions in triple or-statements
#63
DikieDick
closed
1 month ago
0
Merge feature from main: allow for boolean statements in tactics, such as the Assume tactic
#62
jim-portegies
closed
5 months ago
0
Merge 8.17 into main
#61
jim-portegies
closed
5 months ago
0
Wrap types (if needed) before comparing or asserting.
#60
DikieDick
closed
5 months ago
1
feat: Postponing choices in the Choose tactic
#59
jim-portegies
closed
2 months ago
0
[build] Fix use of plugin aliases in findlib loading.
#58
ejgallego
closed
5 months ago
0
Refactor: incorporate some changes from 8.17 and update version numbers
#57
jim-portegies
closed
5 months ago
0
Add test for wp_autorewrite
#56
jim-portegies
closed
5 months ago
0
fix: Change 'Variable' to 'local Parameter'
#55
jim-portegies
closed
5 months ago
0
Testmaster
#54
jim-portegies
closed
5 months ago
0
Adapt to coq/coq#18938 (EConstr.ERelevance)
#53
SkySkimmer
closed
5 months ago
1
Adapt to https://github.com/coq/coq/pull/18880
#52
proux01
closed
6 months ago
2
Specialize
#51
jim-portegies
closed
2 months ago
0
Rewrite the 'match' statement in Since.v to 'match!'
#50
DikieDick
closed
5 months ago
0
Adapt to coq/coq#18624 (Tac2ffi / Tac2val split)
#49
SkySkimmer
closed
8 months ago
2
Adapt to coq/coq#18546.
#48
rlepigre
closed
6 months ago
1
Adapt to coq/coq#18529 (no Dyn.anonymous)
#47
SkySkimmer
closed
8 months ago
1
Merge features of version 2.1.1 into coq-master
#46
jim-portegies
closed
9 months ago
0
fix: Compatibility with compilers >= 4.09.0
#45
jim-portegies
closed
9 months ago
0
feat: create option to print rewrite hints
#44
jim-portegies
closed
9 months ago
0
feat: add logging sentence for wp_autorewrite
#43
jim-portegies
closed
9 months ago
0
The VsCode pluging does not seem to uninstall properly
#42
jnarboux
closed
10 months ago
1
Adapt to coq/coq#18327 (projection opacity)
#41
rlepigre
closed
8 months ago
3
Problem installing using opam
#40
jnarboux
closed
9 months ago
4
Install instruction in VsCode plugin
#39
jnarboux
closed
1 month ago
3
Fix for problems with strong induction for defining index sequence.
#38
jellooo038
closed
9 months ago
0
Adapt to coq/coq#18280 (case relevance outside case info)
#37
SkySkimmer
closed
11 months ago
2
Set 'Help'-tactic to use default automation system.
#36
jellooo038
closed
11 months ago
0
Next