Hi, for Coq I implemented a setting that dynamically changes proof-shell-end-goals-regexp and thereby either hides or shows additional subgoals (see my commit this morning). If other proof assistants do also want this, we could generalize the change and move the setting into the Proof General menu.
Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
