I am wondering if there's a way to debug proofgeneral on Coq.
Proofgeneral's response time slows down considerably even when I am viewing proof state and simply typing my code. Specifically, when I create a small term, and keep expanding the term by inserting elements in the middle, each element in its own line (trying to create a value of a list-like Inductive type), it takes around 3-4 seconds for each keyboard stroke Enter/Return to be processed as a newline. Granted, my code relies heavily on Coq's Notations, which seems to confuse Proofgeneral. See this.
I believe it's a proofgeneral indentation issue (it sometimes says "Mismatched parentheses").
Is there a way to debug this, or turn off aggressive indentation?
I am wondering if there's a way to debug proofgeneral on Coq.
Proofgeneral's response time slows down considerably even when I am viewing proof state and simply typing my code. Specifically, when I create a small term, and keep expanding the term by inserting elements in the middle, each element in its own line (trying to create a value of a list-like
Inductivetype), it takes around 3-4 seconds for each keyboard strokeEnter/Returnto be processed as a newline. Granted, my code relies heavily on Coq'sNotations, which seems to confuse Proofgeneral. See this.I believe it's a proofgeneral indentation issue (it sometimes says "Mismatched parentheses").
Is there a way to debug this, or turn off aggressive indentation?