issues
search
mit-plv
/
fiat
Mostly Automated Synthesis of Correct-by-Construction Programs
http://plv.csail.mit.edu/fiat/
Other
147
stars
31
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
adapt to coq/coq#15220
#62
gares
closed
2 years ago
4
Prepare for 8.16
#61
SkySkimmer
closed
2 years ago
0
[CI] Update Coq versions
#60
JasonGross
closed
2 years ago
0
Adapt w.r.t. coq/coq#15159.
#59
ppedrot
closed
2 years ago
1
Adapt to coq/coq#14986 (setoid_rewrite nondep assumptions under binders)
#58
SkySkimmer
closed
2 years ago
0
Adapt to coq/coq#14819
#57
proux01
closed
3 years ago
0
Update coq-script submodule
#56
proux01
closed
3 years ago
0
Adapt to coq/coq#14705 (hints.ml has its own locality type instead of reusing option locality)
#55
SkySkimmer
closed
3 years ago
1
Adapt w.r.t. coq/coq#14684
#54
ppedrot
closed
3 years ago
4
Speed up morphism search of setoid-rewrite
#53
mattam82
closed
3 years ago
10
Backwards compatible fix for pr 13969: perf issues with setoid-rewrite
#52
mattam82
closed
3 years ago
0
Split off v8.14 files for https://github.com/mit-plv/fiat/pull/50
#51
JasonGross
closed
3 years ago
0
ML code compatibility for Coq PR # 6285
#50
mattam82
closed
1 year ago
6
Hopefully compat with coq/coq#13741: remove omega
#49
JasonGross
closed
3 years ago
0
Adapt to removal of Bracketing Last Introduction Pattern flag.
#48
herbelin
closed
3 years ago
7
Implicit arguments were formerly inactive in "Context".
#47
herbelin
closed
3 years ago
0
Adapt to coq/coq#13188 (Default disable automatic generalization of Instance type)
#46
SkySkimmer
closed
3 years ago
0
Adapt w.r.t. coq/coq#13139.
#45
ppedrot
closed
3 years ago
4
Adapt w.r.t. coq/coq#12977.
#44
ppedrot
closed
3 years ago
1
Adapting to Coq PR#12960: implicit arguments not any more lost when nesting applicative notations
#43
herbelin
closed
4 years ago
0
ijcar2020 branch fails to build
#42
paul-snively
closed
4 years ago
5
Fix w.r.t. coq/coq#12493.
#41
ppedrot
closed
4 years ago
4
Adapt w.r.t. coq/coq#12505.
#40
ppedrot
closed
4 years ago
3
[coq] use ListNotations explicitly
#39
llelf
closed
4 years ago
3
overlay for coq/coq#12162
#38
olaure01
closed
4 years ago
0
Update .travis.yml
#37
JasonGross
closed
4 years ago
0
Fail to make querystructures on Coq > 8.9
#36
sqrta
opened
4 years ago
2
Fix w.r.t. coq/coq#11812.
#35
ppedrot
closed
4 years ago
2
Explicit which hint databases to use with “firstorder”
#34
vbgl
closed
4 years ago
1
Adapt to the removal of the Template Check option.
#33
ppedrot
closed
4 years ago
0
Adapt to coq/coq#11368 (Turn trailing implicit warning into an error)
#32
SimonBoulier
closed
4 years ago
2
Having @ in front of a notation variable was tolerated but is now an error
#31
herbelin
closed
4 years ago
0
[coq] Please update the repository for Coq 8.12
#30
ejgallego
closed
4 years ago
1
[parsers] Avoid relying on `Export` bugs
#29
maximedenes
closed
5 years ago
0
Add -no-template-check until template inductive types are defined
#28
mattam82
closed
5 years ago
6
Adapting to Coq PR#8726.
#27
herbelin
closed
5 years ago
2
[coq] Fix more warnings.
#26
ejgallego
closed
5 years ago
0
[coq] Fix OCaml warnings.
#25
ejgallego
closed
5 years ago
0
[warnings] Please fix OCaml warnings
#24
ejgallego
closed
5 years ago
1
Make trivial instances explicit
#23
maximedenes
closed
5 years ago
0
Fix more occurrences of Instance with partial terms
#22
maximedenes
closed
5 years ago
0
Fix ML4_OR_MLG
#21
SkySkimmer
closed
5 years ago
7
Do not rely on `Refine Instance Mode`
#20
maximedenes
closed
5 years ago
0
[coq] Adapt to coq/coq#9173
#19
ejgallego
closed
5 years ago
4
Drop support for master,trunk (master is now v8.10)
#18
JasonGross
closed
5 years ago
1
Port Fiat to coqpp
#17
ppedrot
closed
5 years ago
4
Adapt to coq/coq#8844 (move abstract out of tactics.ml)
#16
SkySkimmer
closed
5 years ago
2
Don't use ltac_apply, use Tacinterp.Value.apply
#15
JasonGross
closed
5 years ago
0
[Coq 8.9+] Please fix deprecation warnings in 8.9
#14
ejgallego
closed
5 years ago
14
Please make fiat-parsers compile with -w "+compatibility-notation"
#13
Zimmi48
closed
6 years ago
0
Previous
Next