Hjalte Sorgenfrei Mac Dalland (Mar 14 2023 at 09:46): Hjalte Sorgenfrei Mac Dalland (Mar 14 2023 at 09:46):When we try to get existing lemmas we are currently getting unexpected results, such as the lemma currently being written or lemmas defined later in the same file.
We currently get declarations by doing essentially Search.generic_search (snd (DocumentManager.get_context st pos)).
But this seems to return declarations that does not yet exist in the current enviroments, such as lemmas defined further down the file.
It was my understanding that Document.find_sentence_before and ExecutionManager.get_context should get the state at a particular position in the document.
Hjalte Sorgenfrei Mac Dalland (Apr 11 2023 at 13:13):I made an issue for it at https://github.com/coq-community/vscoq/issues/458
Last updated: Jun 04 2023 at 23:30 UTC