Tej Chajed
Tej Chajed
F* has a special qualifier for KreMLin `[@"substitute"]` that fstar-mode doesn't recognize, so that advancing processes any definitions with this qualifier: ```fstar module Interactive_advance_substitute (* fstar-subp-advance-next here... *) let a...
The current `machine` package doesn't need to be in the Goose repo; it now has a natural home somewhere in its own repo in `goose-lang`, and it can be called...
It seems that coq-serapi will not be maintained after Coq 8.20. How feasible is it to migrate to coqc (adding support for getting the goal) or coq-lsp? I would hate...
- After destructing an equality test, the not equals branch was not simplified. It is now turned into not equals statement over base literals. - word can now make use...
### Is your feature request related to a problem? I use ssreflect rewrite by default, but still fallback to Coq rewrite whenever there's a side condition. This makes me sad...
### Description of the problem Trying to use `-w -overriding-logical-loadpath` followed by `-Q` options that override a subdirectory's logical path still results in a warning. To reproduce, with an empty...
Coq master has slightly tweaked line breaking, which is causing CI to fail. I think we'll just need to have multiple reference outputs and choose the right one based on...
### Summary I'd like to propose adding Linux arm64 as another platform with a binary release. ### Background and Motivation For a course using Dafny, we wanted to tell everyone...
If you process a Require Import, you can backtrack over it with Step Backward, but not with Go to Point.