diff options
Diffstat (limited to 'coq/coq.el')
| -rw-r--r-- | coq/coq.el | 6 |
1 files changed, 5 insertions, 1 deletions
@@ -1362,6 +1362,10 @@ goal is redisplayed." (proof-definvisible coq-unset-printing-synth "Unset Printing Synth.") (proof-definvisible coq-set-printing-coercions "Set Printing Coercions.") (proof-definvisible coq-unset-printing-coercions "Unset Printing Coercions.") +(proof-definvisible coq-set-printing-compact-contexts "Set Printing Compact Contexts.") +(proof-definvisible coq-unset-printing-compact-contexts "Unset Printing Compact Contexts.") +(proof-definvisible coq-set-printing-unfocused "Set Printing Unfocused.") +(proof-definvisible coq-unset-printing-unfocused "Unset Printing Unfocused.") (proof-definvisible coq-set-printing-universes "Set Printing Universes.") (proof-definvisible coq-unset-printing-universes "Unset Printing Universes.") (proof-definvisible coq-set-printing-wildcards "Set Printing Wildcard.") @@ -1666,7 +1670,7 @@ Near here means PT is either inside or just aside of a comment." ;; want xml like tags, and I want them removed before warning display. ;; I want the same for errors -> pgip - proof-shell-eager-annotation-end "\377\\|done\\]\\|</infomsg>\\|\\*\\*\\*\\*\\*\\*\\|) >" ; done + proof-shell-eager-annotation-end coq-shell-eager-annotation-end ; done proof-shell-annotated-prompt-regexp coq-shell-prompt-pattern proof-shell-result-start "\372 Pbp result \373" proof-shell-result-end "\372 End Pbp result \373" |