MackieLoeffel
MackieLoeffel
This PR upstreams the heuristic to locate the right file for projects using `dune` from https://github.com/ProofGeneral/PG/issues/477#issuecomment-999655573. I don't really understand what exactly is going on in `company-coq-library-path` and this PR...
This MR updates the code to lean v4.10.0. This includes changing Std to Batteries and adapting the proofs. This is the first time I am working with Lean, so I...
https://github.com/ProofGeneral/PG/pull/831 breaks jump to definition since it adds additional Show commands, which makes `company-coq--last-output-without-eager-annotation-markers` return the wrong output. This PR fixes this by adding the `'dont-show-when-silent` flag that prevents the...
Calling `org-sql-user-push` with a recent org-ml leads to the error: "Tried to query ’:closed’ for non-existent ’:closed’". I tried debugging it a bit but did not get very far. It...
Based on #107 Add a custom version of synthInstance for the proof mode that can create and instantiate mvars. It is implemented as a simple backtracking search, reusing the standard...
Based on #108 Add support for pure specialization patterns `%h`. This subsumes the dedicated forall specialization parts of proof mode terms. TODO: decide which syntax to use for proof mode...