Issues
- 4
- 5
- 2
elaborate trace mode
#134 opened by briangmilnes - 3
c-c c-r reload better description
#133 opened by briangmilnes - 1
Open not always working
#132 opened by briangmilnes - 0
Not all errors going to *Flycheck errors*
#131 opened by briangmilnes - 17
F* over TRAMP crashes
#102 opened by R1kM - 0
Highlight sladmit
#125 opened by cmovcc - 1
Weird display of the highlighted blocks
#124 opened by beurdouche - 6
fslit seems to no longer work very well
#117 opened by msprotz - 4
can't include file in subdirectory with fslit
#118 opened by msprotz - 2
`nil` confusion
#116 opened by mtzguido - 6
- 6
fstar-debug-invocation and include paths
#93 opened by mtzguido - 5
fstar-mode over docker-tramp
#104 opened by jaybosamiya - 2
- 8
Definition lookup via TAGS
#95 opened by wintersteiger - 4
Missing python script from ELPA installation
#87 opened by jeb2239 - 4
- 1
- 1
- 0
Definition lookup works only once
#97 opened by wintersteiger - 4
No company completion
#103 opened by brettgilio - 5
Using F* remotely, over TRAMP
#98 opened by jaybosamiya - 6
Failure to report proper error location
#92 opened by beurdouche - 13
Individual line comments disrupt interactive mode
#88 opened by parno - 15
Highlight assume/admit?
#91 opened by parno - 3
Uncommenting is possible while F* is busy
#89 opened by jaybosamiya - 22
JSON decoding warnings
#81 opened by nikswamy - 2
decreases clauses
#90 opened by wintersteiger - 6
Ability to use "fstar --indent"
#84 opened by jaybosamiya - 20
C-c C-c does not immediately stop processing
#69 opened by tchajed - 1
Feature request: highlight cheating commands
#66 opened by tchajed - 11
Autocompletion is too eager after in and with
#67 opened by tchajed - 8
Bringing back (* Coq style *) comments
#85 opened by catalin-hritcu - 14
Printing tactics position info
#83 opened by mtzguido - 2
- 11
Pasting causes indentation
#78 opened by kkohbrok - 2
- 5
Can only evaluate once?
#82 opened by catalin-hritcu - 3
- 6
Option to disable all of formatting (like subscript)
#76 opened by ia0 - 2
Synth tactics are run during eager lax checking
#73 opened by tchajed - 3
Printing the goal fails if it has percent signs
#74 opened by tchajed - 1
Collapsing computationally irrelevant code
#72 opened by jkzinzindohoue - 5
Errors from lack of dbus on macOS
#70 opened by tchajed - 1
- 2
Failure("Not an imp") when defining mutually recursive types with refinement and `List.Tot.map`
#65 opened by tahina-pro - 1
- 6