diff options
author | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-01-04 17:14:29 +0100 |
---|---|---|
committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-01-04 17:14:29 +0100 |
commit | 15b977ff32f6c8250d47d7657987b0c94db76710 (patch) | |
tree | 7f70c0855d99fe7d37f784fc45e763ee9afa383b /coq/coq.el | |
parent | af30e1ef04320547273fa02967ddcdb18f380f12 (diff) | |
parent | 8d405f342bb3a1903fc12184f78f191e7d84c29d (diff) |
Merge remote-tracking branch 'OFFICIAL/master'
Diffstat (limited to 'coq/coq.el')
-rw-r--r-- | coq/coq.el | 8 |
1 files changed, 5 insertions, 3 deletions
@@ -1354,6 +1354,8 @@ 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-universes "Set Printing Universes.") +(proof-definvisible coq-unset-printing-universes "Unset Printing Universes.") (proof-definvisible coq-set-printing-wildcards "Set Printing Wildcard.") (proof-definvisible coq-unset-printing-wildcards "Unset Printing Wildcard.") ; Takes an argument @@ -1433,7 +1435,7 @@ Near here means PT is either inside or just aside of a comment." (cond ((coq-looking-at-comment) (coq-get-comment-region (point))) - ((and (looking-back proof-script-comment-end) + ((and (looking-back proof-script-comment-end nil) (save-excursion (forward-char -1) (coq-looking-at-comment))) (coq-get-comment-region (- (point) 1))) ((and (looking-at proof-script-comment-start) @@ -1786,7 +1788,7 @@ Near here means PT is either inside or just aside of a comment." (defpacustom search-blacklist coq-search-blacklist-string "Strings to blacklist in requests to coq environment." :type 'string - ;;:get coq-search-blacklist-string + :get 'coq-get-search-blacklist :setting coq-set-search-blacklist) @@ -1869,7 +1871,7 @@ The not yet delayed output is in the region coq-proof-tree-additional-subgoal-ID-regexp end t) (let ((subgoal-id (match-string-no-properties 1))) (unless (gethash subgoal-id proof-tree-sequent-hash) - (message "CPTGNS new sequent %s found" subgoal-id) + ;; (message "CPTGNS new sequent %s found" subgoal-id) (setq proof-action-list (cons (proof-shell-action-list-item (coq-show-sequent-command subgoal-id) |