From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.org!not-for-mail From: =?UTF-8?Q?Cl=c3=a9ment_Pit--Claudel?= Newsgroups: gmane.emacs.devel Subject: Re: What makes set-window-buffer slow? Date: Fri, 24 Jun 2016 14:31:42 -0400 Message-ID: <576D7C8E.3050803@gmail.com> References: <576C04E4.9040000@gmail.com> <576C2054.3020705@gmail.com> <20160623181242.GB4946@acm.fritz.box> <576C2AAA.1090707@gmail.com> <83fus33ekr.fsf@gnu.org> <576C536A.6060503@gmail.com> <83bn2r2i0y.fsf@gnu.org> <576D2895.4020600@gmail.com> <83shw21yhs.fsf@gnu.org> <576D4160.90201@gmail.com> NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: multipart/signed; micalg=pgp-sha1; protocol="application/pgp-signature"; boundary="OQj6GK6Qj5dgbK1HBkts11r9kohkomv0V" X-Trace: ger.gmane.org 1466794023 26957 80.91.229.3 (24 Jun 2016 18:47:03 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 24 Jun 2016 18:47:03 +0000 (UTC) To: emacs-devel@gnu.org Original-X-From: emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org Fri Jun 24 20:46:55 2016 Return-path: Envelope-to: ged-emacs-devel@m.gmane.org Original-Received: from lists.gnu.org ([208.118.235.17]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1bGW7x-0007HX-Mr for ged-emacs-devel@m.gmane.org; Fri, 24 Jun 2016 20:46:54 +0200 Original-Received: from localhost ([::1]:46813 helo=lists.gnu.org) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1bGW7w-0008AT-Ng for ged-emacs-devel@m.gmane.org; Fri, 24 Jun 2016 14:46:52 -0400 Original-Received: from eggs.gnu.org ([2001:4830:134:3::10]:43397) by lists.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1bGW7e-0004a5-GF for emacs-devel@gnu.org; Fri, 24 Jun 2016 14:46:40 -0400 Original-Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71) (envelope-from ) id 1bGVtJ-0005CI-Nw for emacs-devel@gnu.org; Fri, 24 Jun 2016 14:31:51 -0400 Original-Received: from mout.kundenserver.de ([212.227.126.134]:64267) by eggs.gnu.org with esmtp (Exim 4.71) (envelope-from ) id 1bGVtJ-0005CD-7V for emacs-devel@gnu.org; Fri, 24 Jun 2016 14:31:45 -0400 Original-Received: from [18.26.2.123] ([18.26.2.123]) by mrelayeu.kundenserver.de (mreue002) with ESMTPSA (Nemesis) id 0M4voU-1bZnpR2cow-00zDdF for ; Fri, 24 Jun 2016 20:31:44 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.8.0 In-Reply-To: <576D4160.90201@gmail.com> X-Provags-ID: V03:K0:FWgyugEN6qJV5rdKk6OCybLxl23qCWCVxdQDQFuHapxbLwPX3ig vXXdxN1GeauZk67I95Kg9kThGiGSlxhOJbKcAYegBDJU19q9MQDHMFe8zcedgo0k7ALHdLk YuxVlowCoWV/kxB0eu0WJpCaM+Hlr6PO93maL93Db/g4Xwkt5OxRTUNwSc+rrwx/+QA+ggM MarsiHGuagkldeShhZhNw== X-UI-Out-Filterresults: notjunk:1;V01:K0:/ke9chdDINk=:N6F7qvqSYMf8dUH+V5yWEy IDf0y1sDhbQN5p1f+qhHY1e8zN/e1MJGpMmVp20DN8yyOPvdlhi+9HfFW/9606YvfozFVkPnN dj3UWpFUJJn4T5sE6l69jH2kFcvuUo5po76C1uw0xsPqHQB3Nu7T5rku0p6gt97XuLzsUpTtT kmCbeptN+4/rhKKGby85Xzc2GVn50kSxFuPdHgXsO2/F7NxdykkhLgFwibJNitLdWHoIg2do8 HijNHHmF7p7P0UQujJNyqDUmlNWwoj/Rmt+Fo5sWjab7wSg3W+3Ff9+Ro1mlCnXPnxudWXDy5 O4rmAKIIbm5P0A4GImVp7qtFv88hFIYiOYz8YQIIauPGh9/wVTh3Om07zp1scxHATu+OYly3l PVFhkq5mo6bn+/YoXfmvQkzFXA5sf1V6w/aiJ+QaF4IXNSx3rh88+kOM/0UyWR144zYAGW12c XUWFbNPLcKJm0FYNvf1TQYTSvaNZxX6WiAJJoq3Kk6T/vvefxyw65zKf/B00UZD9XGJhTN/AL ypq2py7UVXR7VYJ18wYK0eDBhb5v7ZK+hTIEWI0j293+HF9kjmxdmmL6Pczn2O7vZidKfxhJ+ zR5kLeMHBATKkz45bGwlSL8T3AGm0fLvbvB779aAb5GpHFXH1Vc1VAkdpiiNAFl1GCpjSuo4d N8CBfuobHmXU/bh7k8rNYBVaUNzsDiS8jiYAnJjE8to6b2PVQ4OiZM9mazW/4264rmkg= X-detected-operating-system: by eggs.gnu.org: GNU/Linux 2.2.x-3.x [generic] X-Received-From: 212.227.126.134 X-BeenThere: emacs-devel@gnu.org X-Mailman-Version: 2.1.21 Precedence: list List-Id: "Emacs development discussions." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: emacs-devel-bounces+ged-emacs-devel=m.gmane.org@gnu.org Original-Sender: "Emacs-devel" Xref: news.gmane.org gmane.emacs.devel:204731 Archived-At: This is an OpenPGP/MIME signed message (RFC 4880 and 3156) --OQj6GK6Qj5dgbK1HBkts11r9kohkomv0V Content-Type: multipart/mixed; boundary="8wjkfrrB5xTsuu5fvb2kRq81hVxxS2oTW" From: =?UTF-8?Q?Cl=c3=a9ment_Pit--Claudel?= To: emacs-devel@gnu.org Message-ID: <576D7C8E.3050803@gmail.com> Subject: Re: What makes set-window-buffer slow? References: <576C04E4.9040000@gmail.com> <576C2054.3020705@gmail.com> <20160623181242.GB4946@acm.fritz.box> <576C2AAA.1090707@gmail.com> <83fus33ekr.fsf@gnu.org> <576C536A.6060503@gmail.com> <83bn2r2i0y.fsf@gnu.org> <576D2895.4020600@gmail.com> <83shw21yhs.fsf@gnu.org> <576D4160.90201@gmail.com> In-Reply-To: <576D4160.90201@gmail.com> --8wjkfrrB5xTsuu5fvb2kRq81hVxxS2oTW Content-Type: multipart/mixed; boundary="------------070201090105060902060102" This is a multi-part message in MIME format. --------------070201090105060902060102 Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable On 2016-06-24 10:19, Cl=E9ment Pit--Claudel wrote: > OK, I'll ask the person who's seeing that bug to generate this report. New report attached. --------------070201090105060902060102 Content-Type: text/plain; charset=UTF-8; name="mergesort-profile4" Content-Transfer-Encoding: quoted-printable Content-Disposition: attachment; filename="mergesort-profile4" [profiler-profile "24.3" cpu #s(hash-table size 487 test equal rehash-siz= e 1.5 rehash-threshold 0.8 data ([let* proof-shell-kill-function kill-buf= fer let progn if if proof-shell-exit progn condition-case progn if if sav= e-current-buffer pg-profile-1 apply] 22 [redisplay let* proof-shell-kill-= function kill-buffer let progn if if proof-shell-exit progn condition-cas= e progn if if save-current-buffer pg-profile-1] 46 [menu-bar-update-buffe= rs redisplay_internal\ \(C\ function\) redisplay progn if let* proof-shel= l-wait catch progn if let* proof-shell-kill-function kill-buffer let prog= n if] 2 [message display-message-or-buffer "#" funcall= shell-command-on-region shell-command if let* progn unwind-protect save-= current-buffer let coq-autodetect-version coq-prog-args funcall cons] 54 = [redisplay progn if let* proof-shell-wait if progn if proof-shell-invisib= le-command let* progn unwind-protect let unwind-protect progn if] 601 [pr= ogn if let* proof-shell-wait if progn if proof-shell-invisible-command le= t* progn unwind-protect let unwind-protect progn if progn] 27 [while prog= n if let* proof-shell-wait if progn if proof-shell-invisible-command let*= progn unwind-protect let unwind-protect progn if] 78 [replace-regexp-in-= string company-coq-trim progn unwind-protect let unwind-protect progn if = progn if company-coq-ask-prover company-coq-unless-error company-coq-ask-= prover-swallow-errors let company-coq-get-all-notations company-coq--list= -to-table] 2 [list let cond let* cond cond let* if company-coq-tg--parse-= tactic-part mapcar company-coq-tg--parse-tactic-subs cons company-coq-tg-= -parse-tactic mapcar let if] 4 [let* company-coq-tg--find-tactics mapcar = apply let cond let* if let* company-coq-tg--find-tactics mapcar apply let= if let* cond] 4 [progn if company-coq-tg--format-tactic let* reverse nco= nc setq while let* condition-case let* company-coq-tg--extract-notations = and let company-coq-get-all-notations company-coq--list-to-table] 8 [redi= splay progn if let* proof-shell-wait if progn if proof-shell-invisible-co= mmand proof-shell-invisible-command-invisible-result mapc if progn if pro= gn unwind-protect] 111 [eval redisplay_internal\ \(C\ function\) redispla= y progn if let* proof-shell-wait if progn if proof-shell-invisible-comman= d "#" mapcar if progn unwind-protect] 3 [redis= play progn if let* proof-shell-wait if progn if proof-shell-invisible-com= mand "#" mapcar if progn unwind-protect progn = if] 355 [progn if let* proof-shell-wait if progn if proof-shell-invisible= -command "#" mapcar if progn unwind-protect pr= ogn if let] 26 [message if pg-hint if pg-response-buffers-hint pg-hint pr= oof-layout-windows proof-multiple-frames-enable progn unwind-protect let = progn unwind-protect save-current-buffer let if] 5 ["#= " funcall syntax-ppss let save-excursion proof-buffer-syntactic-context e= q save-excursion proof-inside-comment or coq-looking-at-comment if coq-fi= nd-comment-start coq-find-not-in-comment-backward let coq-empty-command-p= ] 16 [and setq and while let if coq-script-parse-cmdend-forward coq-scrip= t-parse-function funcall let* while let* save-excursion proof-segment-up-= to let if] 22 ["#" funcall syntax-ppss let save-excurs= ion proof-buffer-syntactic-context eq save-excursion proof-inside-comment= or coq-looking-at-comment if progn if while let] 7 ["#" funcall syntax-ppss let save-excursion proof-buffer-syntactic-context = and or and while let if coq-script-parse-cmdend-forward coq-script-parse-= function funcall let*] 9 ["#" funcall syntax-ppss let= save-excursion proof-buffer-syntactic-context not and if let if coq-scri= pt-parse-cmdend-forward coq-script-parse-function funcall let* while] 10 = [save-excursion proof-inside-comment or coq-looking-at-comment if coq-fin= d-comment-start coq-find-not-in-comment-backward let coq-empty-command-p = not save-excursion and or and while let] 4 [redisplay progn if let* proof= -shell-wait if progn if proof-shell-invisible-command progn if let coq-ad= apt-printing-width run-hooks let proof-assert-until-point] 574 [let and p= roof-re-search-forward-safe cond proof-shell-handle-immediate-output let = proof-shell-filter-manage-output progn if let if if let save-excursion pr= oof-shell-filter progn] 45 [while progn if let* proof-shell-wait if progn= if proof-shell-invisible-command progn if let coq-adapt-printing-width r= un-hooks let proof-assert-until-point] 35 [progn if let* proof-shell-wait= if progn if proof-shell-invisible-command progn if let coq-adapt-printin= g-width run-hooks let proof-assert-until-point if] 28 [while let progn un= wind-protect let let proof-semis-to-vanillas let proof-assert-semis let p= roof-assert-until-point if save-excursion proof-goto-point progn if] 12 [= message map-y-or-n-p save-some-buffers let coq-compile-save-some-buffers = let progn if let while let let if coq-seq-preprocess-require-commands run= -hooks condition-case] 688 [save-some-buffers let coq-compile-save-some-b= uffers let progn if let while let let if coq-seq-preprocess-require-comma= nds run-hooks condition-case proof-extend-queue let] 16 [save-current-buf= fer prog1 unwind-protect let progn unwind-protect let coq-seq-map-module-= id-to-obj-file let coq-seq-check-module while let progn if let while] 18 = ["#" funcall make-temp-file let coq-seq-map-module-id= -to-obj-file let coq-seq-check-module while let progn if let while let le= t if] 19 [nil nil nil nil nil nil nil nil nil nil nil nil nil nil nil nil= ] 64563 [redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil = nil nil nil nil nil nil nil nil] 133 [redisplay--update-region-highlights= apply "#" redisplay_internal\ \(C\ function\) nil nil= nil nil nil nil nil nil nil nil nil nil] 44 [save-current-buffer proof-s= hell-insert proof-shell-insert-action-item if let* save-excursion if proo= f-shell-exec-loop if if let proof-shell-filter-manage-output progn if let= if] 18 [if let coq-last-prompt-info coq-last-prompt-info-safe or let if = coq-set-state-infos run-hooks proof-done-advancing funcall condition-case= proof-shell-invoke-callback mapc let* save-excursion] 53 [proof-done-adv= ancing-comment cond let proof-done-advancing funcall condition-case proof= -shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop = if if let proof-shell-filter-manage-output] 3 ["#" red= isplay--update-region-highlight "#" funcall redisplay-= -update-region-highlights apply "#" redisplay_internal= \ \(C\ function\) nil nil nil nil nil nil nil nil] 15 [and company-coq-bo= undp-string-match-p and let* if company-coq-maybe-proof-input-reload-thin= gs run-hooks let save-current-buffer proof-shell-insert proof-shell-inser= t-action-item if let* save-excursion if proof-shell-exec-loop] 47 [menu-b= ar-update-buffers redisplay_internal\ \(C\ function\) nil nil nil nil nil= nil nil nil nil nil nil nil nil nil] 95 [if eval redisplay_internal\ \(C= \ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 242 [co= ndition-case proof-shell-invoke-callback mapc let* save-excursion if proo= f-shell-exec-loop if if let proof-shell-filter-manage-output progn if let= if if] 6 ["#" funcall redisplay--update-region-highl= ights apply "#" redisplay_internal\ \(C\ function\) ni= l nil nil nil nil nil nil nil nil nil] 24 [span-set-end if proof-make-goa= lsave if let proof-done-advancing-save cond let proof-done-advancing func= all condition-case proof-shell-invoke-callback mapc let* save-excursion i= f] 6 [apply "#" redisplay_internal\ \(C\ function\) ni= l nil nil nil nil nil nil nil nil nil nil nil nil] 149 [eval redisplay_in= ternal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil n= il nil] 235 [proof-set-locked-endpoints if proof-set-locked-end let proof= -done-advancing funcall condition-case proof-shell-invoke-callback mapc l= et* save-excursion if proof-shell-exec-loop if if let] 439 [let proof-str= ing-match and cond progn if while let proof-done-advancing-save cond let = proof-done-advancing funcall condition-case proof-shell-invoke-callback m= apc] 90 [if let* let scomint-send-input let save-current-buffer proof-she= ll-insert proof-shell-insert-action-item if let* save-excursion if proof-= shell-exec-loop if if let] 83 [progn if let if let company-coq-state-chan= ge run-hooks proof-done-advancing funcall condition-case proof-shell-invo= ke-callback mapc let* save-excursion if proof-shell-exec-loop] 60 [file-r= emote-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil n= il nil nil nil nil nil nil] 476 [keymap-canonicalize redisplay_internal\ = \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil nil] = 45 [proof-shell-handle-immediate-output let proof-shell-filter-manage-out= put progn if let if if let save-excursion proof-shell-filter progn condit= ion-case while let if] 7 [proof-shell-live-buffer and proof-toolbar-comma= nd-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil n= il nil nil nil nil nil] 4 [and setq while let coq-search-urgent-message s= etq and while let proof-shell-process-urgent-messages and save-excursion = proof-shell-filter progn condition-case while] 47 [save-excursion set-mar= ker and proof-set-overlay-arrow proof-set-locked-endpoints if proof-set-l= ocked-end let proof-done-advancing funcall condition-case proof-shell-inv= oke-callback mapc let* save-excursion if] 361 [if save-excursion set-mark= er and proof-set-overlay-arrow proof-set-locked-endpoints if proof-set-lo= cked-end let proof-done-advancing funcall condition-case proof-shell-invo= ke-callback mapc let* save-excursion] 51 [proof-shell-insert proof-shell-= insert-action-item if let* save-excursion if proof-shell-exec-loop if if = let proof-shell-filter-manage-output progn if let if if] 42 [let progn if= let span-at-before prev-span setq while let proof-done-advancing-save co= nd let proof-done-advancing funcall condition-case proof-shell-invoke-cal= lback] 12 [if save-excursion if proof-shell-exec-loop if if let proof-she= ll-filter-manage-output progn if let if if let save-excursion proof-shell= -filter] 27 [run-hooks let save-current-buffer proof-shell-insert proof-s= hell-insert-action-item if let* save-excursion if proof-shell-exec-loop i= f if let proof-shell-filter-manage-output progn if] 2 [proof-shell-filter= -wrapper run-hook-with-args let save-current-buffer progn if let scomint-= output-filter nil nil nil nil nil nil nil nil] 3 [facep or if let* pg-set= -span-helphighlights let proof-done-advancing-other cond let proof-done-a= dvancing funcall condition-case proof-shell-invoke-callback mapc let* sav= e-excursion] 5 [if let if if let save-excursion proof-shell-filter progn = condition-case while let if proof-shell-filter-wrapper run-hook-with-args= let save-current-buffer] 28 [span-delete if while let proof-done-advanci= ng-save cond let proof-done-advancing funcall condition-case proof-shell-= invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 101 [m= ap-keymap keymap-canonicalize redisplay_internal\ \(C\ function\) nil nil= nil nil nil nil nil nil nil nil nil nil nil] 14 [funcall condition-case = proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-= loop if if let proof-shell-filter-manage-output progn if let if] 12 [and = proof-shell-live-buffer and proof-shell-available-p and progn cond proof-= toolbar-undo-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil= nil nil nil] 6 [if let if coq-set-state-infos run-hooks proof-done-advan= cing funcall condition-case proof-shell-invoke-callback mapc let* save-ex= cursion if proof-shell-exec-loop if if] 40 [let if build-list-id-from-str= ing let progn if let coq-last-prompt-info coq-last-prompt-info-safe or le= t if coq-set-state-infos run-hooks proof-done-advancing funcall] 12 [imag= e-search-load-path find-image eval "#" mapcar tool-bar= -make-keymap-1 tool-bar-make-keymap redisplay_internal\ \(C\ function\) n= il nil nil nil nil nil nil nil] 19 [and proof-toolbar-context-enable-p re= display_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil= nil nil nil] 13 [set-marker and proof-set-overlay-arrow proof-set-locked= -endpoints if proof-set-locked-end let proof-done-advancing funcall condi= tion-case proof-shell-invoke-callback mapc let* save-excursion if proof-s= hell-exec-loop] 13 [let* pg-set-span-helphighlights let proof-done-advanc= ing-other cond let proof-done-advancing funcall condition-case proof-shel= l-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if] 1= 6 [setq let* save-excursion if proof-shell-exec-loop if if let proof-shel= l-filter-manage-output progn if let if if let save-excursion] 11 [save-ex= cursion proof-locked-region-full-p not progn cond proof-toolbar-next-enab= le-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil = nil] 4 [let proof-string-match and while let coq-count-match let* coq-mod= ule-opening-p or let or coq-goal-command-p funcall cond let proof-done-ad= vancing-other] 9 [string-equal not or if pg-add-to-input-history if let p= roof-done-advancing funcall condition-case proof-shell-invoke-callback ma= pc let* save-excursion if proof-shell-exec-loop] 17 [proof-done-advancing= funcall condition-case proof-shell-invoke-callback mapc let* save-excurs= ion if proof-shell-exec-loop if if let proof-shell-filter-manage-output p= rogn if let] 21 [redisplay--update-region-highlight "#" funcall redisplay--update-region-highlights apply "#" redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil ni= l] 28 [let* save-excursion if proof-shell-exec-loop if if let proof-shell= -filter-manage-output progn if let if if let save-excursion proof-shell-f= ilter] 11 [let proof-done-advancing funcall condition-case proof-shell-in= voke-callback mapc let* save-excursion if proof-shell-exec-loop if if let= proof-shell-filter-manage-output progn if] 33 [eq if let span-at-before = prev-span setq while let proof-done-advancing-save cond let proof-done-ad= vancing funcall condition-case proof-shell-invoke-callback mapc] 5 [not a= nd if let* save-excursion if proof-shell-exec-loop if if let proof-shell-= filter-manage-output progn if let if if] 2 [+ let* coq-module-opening-p o= r let or coq-goal-command-p funcall cond progn if while let proof-done-ad= vancing-save cond let] 3 [and if let if pg-processing-complete-hint if if= let* save-excursion if proof-shell-exec-loop if if let proof-shell-filte= r-manage-output progn] 254 [cond proof-retract-buffer funcall progn unwin= d-protect let if save-current-buffer let proof-protected-process-or-retra= ct if let* save-current-buffer if proof-deactivate-scripting progn] 8 [if= progn if progn if let progn unwind-protect save-current-buffer let save-= excursion if proof-display-and-keep-buffer pg-response-display if proof-s= hell-display-output-as-response] 4 [redisplay progn if let* proof-shell-w= ait progn unwind-protect let if save-current-buffer let proof-protected-p= rocess-or-retract if let* save-current-buffer if] 1928 [progn if let* pro= of-shell-wait progn unwind-protect let if save-current-buffer let proof-p= rotected-process-or-retract if let* save-current-buffer if proof-deactiva= te-scripting] 131 [redisplay progn if let* proof-shell-wait catch progn i= f let* proof-shell-kill-function kill-buffer let progn if if proof-shell-= exit] 57 [span-delete-spans proof-script-delete-spans save-current-buffer= if save-excursion "#" mapcar proof-restart-bu= ffers proof-script-remove-all-spans-and-deactivate let* proof-shell-kill-= function kill-buffer let progn if if] 2 [span-delete mapc span-mapc-spans= span-delete-spans proof-script-delete-secondary-spans save-current-buffe= r if save-excursion "#" mapcar proof-restart-b= uffers proof-script-remove-all-spans-and-deactivate let* proof-shell-kill= -function kill-buffer let] 22 [while let save-current-buffer proof-shell-= config-done coq-shell-mode-config let progn delay-mode-hooks coq-shell-mo= de funcall save-current-buffer let if proof-shell-start proof-shell-ready= -prover condition-case] 20 [unwind-protect let unwind-protect progn if pr= ogn if company-coq-ask-prover let* progn if company-coq-ask-prover-redire= ct car let* progn if] 7 [while while let* progn unwind-protect save-curre= nt-buffer let company-coq-tg--preprocess-tactics-grammar let* company-coq= -tg--extract-notations and let company-coq-get-all-notations company-coq-= -list-to-table setq company-coq-tactic-initialize-notations-filter] 30 [i= f company-coq-tg--parse-tactic-part mapcar company-coq-tg--parse-tactic-s= ubs cons company-coq-tg--parse-tactic mapcar let if let* if company-coq-t= g--parse-group cons let cond let*] 92 [setq if while let* company-coq--sp= lit-seq mapcar company-coq-tg--parse-tactic-subs cons company-coq-tg--par= se-tactic mapcar let if let* if company-coq-tg--parse-group cons] 4 [let = "#" funcall cond let* cond let* company-coq-tg= --format-tactic-rec progn if company-coq-tg--format-tactic let* reverse n= conc setq while] 4 [setq while let progn unwind-protect let let proof-sem= is-to-vanillas let proof-assert-semis let proof-assert-until-point if sav= e-excursion proof-goto-point progn] 11 [apply setq progn unwind-protect s= ave-current-buffer let let coq-seq-get-library-dependencies setq progn un= wind-protect let coq-seq-map-module-id-to-obj-file let coq-seq-check-modu= le while] 8 [and unwind-protect save-current-buffer let let coq-seq-get-l= ibrary-dependencies setq progn unwind-protect let coq-seq-map-module-id-t= o-obj-file let coq-seq-check-module while let progn] 83 [if let* let scom= int-send-input let save-current-buffer proof-shell-insert proof-shell-ins= ert-action-item progn if progn if let proof-add-to-queue proof-extend-que= ue let] 3 [tool-bar-make-keymap redisplay_internal\ \(C\ function\) nil n= il nil nil nil nil nil nil nil nil nil nil nil nil] 72 [coq-last-prompt-i= nfo coq-last-prompt-info-safe or let if coq-set-state-infos run-hooks pro= of-done-advancing funcall condition-case proof-shell-invoke-callback mapc= let* save-excursion if proof-shell-exec-loop] 15 [display-graphic-p if e= val redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil n= il nil nil nil] 25 [let* pg-add-element cond let proof-done-advancing-oth= er cond let proof-done-advancing funcall condition-case proof-shell-invok= e-callback mapc let* save-excursion if proof-shell-exec-loop] 18 [if proo= f-shell-exec-loop if if let proof-shell-filter-manage-output progn if let= if if let save-excursion proof-shell-filter progn condition-case] 30 ["#= " mapcar tool-bar-make-keymap-1 tool-bar-make-keymap r= edisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil ni= l nil] 4 [list list let* pg-add-element cond let proof-done-advancing-oth= er cond let proof-done-advancing funcall condition-case proof-shell-invok= e-callback mapc let* save-excursion] 1 [save-excursion if proof-shell-exe= c-loop if if let proof-shell-filter-manage-output progn if let if if let = save-excursion proof-shell-filter progn] 14 [setq if let save-current-buf= fer proof-shell-insert proof-shell-insert-action-item if let* save-excurs= ion if proof-shell-exec-loop if if let proof-shell-filter-manage-output p= rogn] 13 [ring-index ring-ref string-equal not or if pg-add-to-input-hist= ory if let proof-done-advancing funcall condition-case proof-shell-invoke= -callback mapc let* save-excursion] 3 [let progn if let coq-last-prompt-i= nfo coq-last-prompt-info-safe or let if coq-set-state-infos run-hooks pro= of-done-advancing funcall condition-case proof-shell-invoke-callback mapc= ] 22 [let save-current-buffer progn if let scomint-output-filter nil nil = nil nil nil nil nil nil nil nil] 40 [let if let spans-at-point-prop car-s= afe span-at save-current-buffer proof-last-locked-span if let if coq-set-= state-infos run-hooks proof-done-advancing funcall condition-case] 23 [if= let if build-list-id-from-string let progn if let coq-last-prompt-info c= oq-last-prompt-info-safe or let if coq-set-state-infos run-hooks proof-do= ne-advancing] 5 [or if pg-add-to-input-history if let proof-done-advancin= g funcall condition-case proof-shell-invoke-callback mapc let* save-excur= sion if proof-shell-exec-loop if if] 4 [save-excursion let* pg-set-span-h= elphighlights let proof-done-advancing-other cond let proof-done-advancin= g funcall condition-case proof-shell-invoke-callback mapc let* save-excur= sion if proof-shell-exec-loop] 53 [and cond progn if while let proof-done= -advancing-save cond let proof-done-advancing funcall condition-case proo= f-shell-invoke-callback mapc let* save-excursion] 5 [let proof-shell-proc= ess-urgent-messages and save-excursion proof-shell-filter progn condition= -case while let if proof-shell-filter-wrapper run-hook-with-args let save= -current-buffer progn if] 10 [let scomint-check-proc and proof-shell-live= -buffer and proof-toolbar-state-enable-p redisplay_internal\ \(C\ functio= n\) nil nil nil nil nil nil nil nil nil] 7 [save-current-buffer progn if = let scomint-output-filter nil nil nil nil nil nil nil nil nil nil nil] 14= [and proof-shell-live-buffer and proof-toolbar-state-enable-p redisplay_= internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil] 13= [set-marker if let save-current-buffer proof-shell-insert proof-shell-in= sert-action-item if let* save-excursion if proof-shell-exec-loop if if le= t proof-shell-filter-manage-output progn] 8 [coq-get-span-proofnum or if = let if coq-set-state-infos run-hooks proof-done-advancing funcall conditi= on-case proof-shell-invoke-callback mapc let* save-excursion if proof-she= ll-exec-loop] 3 [mode-line-eol-desc eval redisplay_internal\ \(C\ functio= n\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 8 [cond proof-to= olbar-next-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil n= il nil nil nil nil nil nil nil nil] 167 [every or and let* save-excursion= if proof-shell-exec-loop if if let proof-shell-filter-manage-output prog= n if let if if] 6 [or proof-unprocessed-begin - span-at save-current-buff= er proof-last-locked-span if let if coq-set-state-infos run-hooks proof-d= one-advancing funcall condition-case proof-shell-invoke-callback mapc] 15= [coq-section-command-p or let or coq-goal-command-p funcall cond progn i= f while let proof-done-advancing-save cond let proof-done-advancing funca= ll] 9 [concat proof-element-id proof-next-element-id let proof-done-advan= cing-other cond let proof-done-advancing funcall condition-case proof-she= ll-invoke-callback mapc let* save-excursion if proof-shell-exec-loop] 17 = [let if coq-show-first-goal run-hooks let proof-shell-handle-delayed-outp= ut setq if if let proof-shell-filter-manage-output progn if let if if] 3 = [progn unwind-protect let if save-current-buffer let proof-protected-proc= ess-or-retract if let* save-current-buffer if proof-deactivate-scripting = progn condition-case proof-deactivate-scripting-auto catch] 3 [progn cond= ition-case setq progn while let* progn unwind-protect save-current-buffer= let company-coq-tg--preprocess-tactics-grammar let* company-coq-tg--extr= act-notations and let company-coq-get-all-notations] 110 [let* company-co= q--split-seq mapcar company-coq-tg--parse-tactic-subs cons company-coq-tg= --parse-tactic mapcar let if let* if company-coq-tg--parse-group cons let= cond let*] 4 [let "#" funcall cond let* cond = let* company-coq-tg--format-tactic-rec let* let "#" funcall cond let* cond let*] 8 [while progn if let* proof-shell-wait= if progn if proof-shell-invisible-command "#"= mapcar if progn unwind-protect progn if] 2 [window--pixel-to-total byte-= code split-window split-window-horizontally cond progn unwind-protect sav= e-current-buffer let let proof-select-three-b save-excursion progn if pro= of-display-three-b cond] 3 [menu-bar-update-buffers redisplay_internal\ \= (C\ function\) message map-y-or-n-p save-some-buffers let coq-compile-sav= e-some-buffers let progn if let while let let if coq-seq-preprocess-requi= re-commands] 5 [proof-string-match and while let coq-count-match let* coq= -module-opening-p or let or coq-goal-command-p funcall cond let proof-don= e-advancing-other cond] 6 [if if let save-excursion proof-shell-filter pr= ogn condition-case while let if proof-shell-filter-wrapper run-hook-with-= args let save-current-buffer progn if] 1 [proof-locked-region-full-p not = progn cond proof-toolbar-next-enable-p redisplay_internal\ \(C\ function\= ) nil nil nil nil nil nil nil nil nil nil] 56 [null or and if let* save-e= xcursion if proof-shell-exec-loop if if let proof-shell-filter-manage-out= put progn if let if] 6 [let proof-string-match and let proof-get-name-fro= m-goal or setq if let proof-done-advancing-save cond let proof-done-advan= cing funcall condition-case proof-shell-invoke-callback] 18 [if let span-= at-before prev-span setq while let proof-done-advancing-save cond let pro= of-done-advancing funcall condition-case proof-shell-invoke-callback mapc= let*] 15 [proof-re-search-forward-safe cond proof-shell-handle-immediate= -output let proof-shell-filter-manage-output progn if let if if let save-= excursion proof-shell-filter progn condition-case while] 6 [let coq-last-= prompt-info coq-last-prompt-info-safe or let if coq-set-state-infos run-h= ooks proof-done-advancing funcall condition-case proof-shell-invoke-callb= ack mapc let* save-excursion if] 8 [framep-on-display display-graphic-p i= f eval redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil ni= l nil nil nil] 8 [progn if let coq-last-prompt-info coq-last-prompt-info-= safe or let if coq-set-state-infos run-hooks proof-done-advancing funcall= condition-case proof-shell-invoke-callback mapc let*] 19 [unless eval re= display_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil= nil nil nil] 236 [eq proof-locked-region-empty-p not progn cond proof-to= olbar-retract-enable-p redisplay_internal\ \(C\ function\) nil nil nil ni= l nil nil nil nil nil] 7 [if proof-set-locked-end let proof-done-advancin= g funcall condition-case proof-shell-invoke-callback mapc let* save-excur= sion if proof-shell-exec-loop if if let proof-shell-filter-manage-output]= 32 [company-coq-state-change run-hooks proof-done-advancing funcall cond= ition-case proof-shell-invoke-callback mapc let* save-excursion if proof-= shell-exec-loop if if let proof-shell-filter-manage-output progn] 2 [let = coq-count-match let* coq-module-opening-p or let or coq-goal-command-p fu= ncall cond let proof-done-advancing-other cond let proof-done-advancing f= uncall] 7 [let* coq-module-opening-p or let or coq-goal-command-p funcall= cond progn if while let proof-done-advancing-save cond let proof-done-ad= vancing] 5 [progn pg-add-element cond let proof-done-advancing-other cond= let proof-done-advancing funcall condition-case proof-shell-invoke-callb= ack mapc let* save-excursion if proof-shell-exec-loop] 2 [let proof-done-= advancing-other cond let proof-done-advancing funcall condition-case proo= f-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop= if if let] 8 [let proof-string-match if proof-string-match-safe and cond= let proof-done-advancing funcall condition-case proof-shell-invoke-callb= ack mapc let* save-excursion if proof-shell-exec-loop] 17 [proof-string-m= atch and while let coq-count-match let* coq-module-opening-p or let or co= q-goal-command-p funcall cond progn if while] 17 [eq cond let proof-done-= advancing funcall condition-case proof-shell-invoke-callback mapc let* sa= ve-excursion if proof-shell-exec-loop if if let proof-shell-filter-manage= -output] 5 [proof-element-id proof-next-element-id let proof-done-advanci= ng-other cond let proof-done-advancing funcall condition-case proof-shell= -invoke-callback mapc let* save-excursion if proof-shell-exec-loop if] 10= [- max if set-marker let proof-shell-process-urgent-messages and save-ex= cursion proof-shell-filter progn condition-case while let if proof-shell-= filter-wrapper run-hook-with-args] 5 [cond proof-shell-handle-immediate-o= utput let proof-shell-filter-manage-output progn if let if if let save-ex= cursion proof-shell-filter progn condition-case while let] 3 [let proof-s= tring-match and while let coq-count-match + let* coq-module-opening-p or = let or coq-goal-command-p funcall cond progn] 4 [pg-remove-element "#" funcall "#" mapc span-delete= if while let proof-done-advancing-save cond let proof-done-advancing fun= call condition-case proof-shell-invoke-callback] 6 [internal--after-with-= selected-window unwind-protect save-current-buffer let let progn if progn= unwind-protect let let progn if if coq-optimise-resp-windows progn] 7 [i= f while let if let spans-at-region-prop mapc span-mapc-spans span-delete-= spans proof-script-delete-spans let if proof-done-retracting funcall cond= ition-case proof-shell-invoke-callback] 4 [apply let* tramp-completion-ru= n-real-handler if let tramp-completion-file-name-handler file-symlink-p f= ile-truename apply let* tramp-completion-run-real-handler if let tramp-co= mpletion-file-name-handler file-truename file-truename] 2 [byte-code dele= te-window delete-windows-on progn if while let let let* proof-shell-kill-= function kill-buffer let progn if if proof-shell-exit] 13 [if coq-set-sta= te-infos run-hooks proof-grab-lock progn if progn if let proof-add-to-que= ue proof-start-queue let* progn if proof-shell-invisible-command let*] 3 = [cond let* cond cond let* if company-coq-tg--parse-tactic-part mapcar com= pany-coq-tg--parse-tactic-subs cons company-coq-tg--parse-tactic mapcar l= et if let* if] 4 [company-coq--split-seq mapcar company-coq-tg--parse-tac= tic-subs cons company-coq-tg--parse-tactic mapcar let if let* if company-= coq-tg--parse-group cons let cond let* if] 153 [cond let* if company-coq-= tg--parse-tactic-part mapcar company-coq-tg--parse-tactic-subs cons compa= ny-coq-tg--parse-tactic mapcar let if let* if company-coq-tg--parse-group= cons let] 2 [cons setq while let* reverse nconc setq while let* let "#" funcall cond let* cond let*] 5 [company-coq-tg= --format-tactic-rec let "#" funcall cond let* = cond let* company-coq-tg--format-tactic-rec progn if company-coq-tg--form= at-tactic let* reverse nconc setq] 4 [let coq-last-prompt-info coq-last-p= rompt-info-safe or let if coq-set-state-infos run-hooks proof-done-invisi= ble funcall condition-case proof-shell-invoke-callback mapc let* save-exc= ursion if] 7 [let* progn if while let progn unwind-protect let let proof-= semis-to-vanillas let proof-assert-semis let proof-assert-until-point if = save-excursion] 9 [while let let if coq-seq-preprocess-require-commands r= un-hooks condition-case proof-extend-queue let proof-assert-semis let pro= of-assert-until-point if save-excursion proof-goto-point progn] 150 [file= -name-sans-extension x-gtk-map-stock redisplay_internal\ \(C\ function\) = nil nil nil nil nil nil nil nil nil nil nil nil nil] 5 [eq if save-excurs= ion set-marker and proof-set-overlay-arrow proof-set-locked-endpoints if = proof-set-locked-end let proof-done-advancing funcall condition-case proo= f-shell-invoke-callback mapc let*] 1 [progn if let scomint-output-filter = nil nil nil nil nil nil nil nil nil nil nil nil] 18 [or if let if coq-set= -state-infos run-hooks proof-done-advancing funcall condition-case proof-= shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loop i= f] 5 [or coq-goal-command-p funcall cond let proof-done-advancing-other c= ond let proof-done-advancing funcall condition-case proof-shell-invoke-ca= llback mapc let* save-excursion if] 3 [let* if company-coq-maybe-proof-in= put-reload-things run-hooks let save-current-buffer proof-shell-insert pr= oof-shell-insert-action-item if let* save-excursion if proof-shell-exec-l= oop if if let] 9 [let* let scomint-send-input let save-current-buffer pro= of-shell-insert proof-shell-insert-action-item if let* save-excursion if = proof-shell-exec-loop if if let proof-shell-filter-manage-output] 6 [proo= f-debug if proof-done-advancing-save cond let proof-done-advancing funcal= l condition-case proof-shell-invoke-callback mapc let* save-excursion if = proof-shell-exec-loop if if] 9 [if progn if pg-add-to-input-history if le= t proof-done-advancing funcall condition-case proof-shell-invoke-callback= mapc let* save-excursion if proof-shell-exec-loop if] 12 [mapc let* save= -excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-o= utput progn if let if if let save-excursion] 4 [and while let coq-count-m= atch let* coq-module-opening-p or let or coq-goal-command-p funcall cond = let proof-done-advancing-other cond let] 1 [let proof-string-match and wh= ile let coq-count-match + let* coq-module-opening-p or let or coq-goal-co= mmand-p funcall cond let] 12 [let* coq-module-opening-p or let or coq-goa= l-command-p funcall cond let proof-done-advancing-other cond let proof-do= ne-advancing funcall condition-case proof-shell-invoke-callback] 6 [let p= roof-done-advancing-save cond let proof-done-advancing funcall condition-= case proof-shell-invoke-callback mapc let* save-excursion if proof-shell-= exec-loop if if let] 4 [proof-shell-filter-manage-output progn if let if = if let save-excursion proof-shell-filter progn condition-case while let i= f proof-shell-filter-wrapper run-hook-with-args] 9 [timer-relative-time t= imer-inc-time timer-event-handler nil nil nil nil nil nil nil nil nil nil= nil nil nil] 13 [if if let* let scomint-send-input let save-current-buff= er proof-shell-insert proof-shell-insert-action-item if let* save-excursi= on if proof-shell-exec-loop if if] 8 [progn cond proof-toolbar-qed-enable= -p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil ni= l nil nil nil] 2 [let* pg-remove-element "#" fu= ncall "#" mapc span-delete if while let proof-done-a= dvancing-save cond let proof-done-advancing funcall condition-case] 8 [le= t coq-count-match let* coq-module-opening-p or let or coq-goal-command-p = funcall cond progn if while let proof-done-advancing-save cond] 4 [and le= t* if company-coq-maybe-proof-input-reload-things run-hooks let save-curr= ent-buffer proof-shell-insert proof-shell-insert-action-item if let* save= -excursion if proof-shell-exec-loop if if] 6 [while progn if let* proof-s= hell-wait progn unwind-protect let if save-current-buffer let proof-prote= cted-process-or-retract if let* save-current-buffer if] 7 [while let catc= h progn if let* proof-shell-kill-function kill-buffer let progn if if pro= of-shell-exit progn condition-case progn] 21 [apply start-file-process ap= ply setq let let scomint-exec-1 if let save-current-buffer scomint-exec i= f scomint-make-in-buffer apply scomint-make apply] 2 [let progn condition= -case company-coq-read-and-delete cons let* progn if company-coq-ask-prov= er-redirect car let* progn if company-coq-detect-capabilities progn if] 5= [setq while let* company-coq--split-seq mapcar let if let* if company-co= q-tg--parse-group cons let cond let* if cond] 4 [progn if while let* comp= any-coq--split-seq mapcar company-coq-tg--parse-tactic-subs cons company-= coq-tg--parse-tactic mapcar let if let* if company-coq-tg--parse-group co= ns] 3 [company-coq-tg--mk-placeholder list list cond let cond let* compan= y-coq-tg--format-tactic-rec let "#" funcall co= nd let* cond let* company-coq-tg--format-tactic-rec] 13 [setq while let* = let company-coq--list-to-table setq company-coq-tactic-initialize-notatio= ns-filter progn if company-coq-prover-init run-hooks progn unwind-protect= progn if let] 4 [menu-bar-update-buffers-1 menu-bar-update-buffers redis= play_internal\ \(C\ function\) redisplay progn if let* proof-shell-wait i= f progn if proof-shell-invisible-command "#" m= apcar if progn] 2 [internal--after-with-selected-window unwind-protect sa= ve-current-buffer let + - let progn if progn unwind-protect let let progn= if if] 3 [map-y-or-n-p save-some-buffers let coq-compile-save-some-buffe= rs let progn if let while let let if coq-seq-preprocess-require-commands = run-hooks condition-case proof-extend-queue] 29 [mapconcat let while let = let if coq-seq-preprocess-require-commands run-hooks condition-case proof= -extend-queue let proof-assert-semis let proof-assert-until-point if save= -excursion] 4 [apply if let save-current-buffer proof-shell-insert proof-= shell-insert-action-item if let* save-excursion if proof-shell-exec-loop = if if let proof-shell-filter-manage-output progn] 4 [cond proof-toolbar-q= ed-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil n= il nil nil nil nil nil nil] 3 [if let proof-done-advancing funcall condit= ion-case proof-shell-invoke-callback mapc let* save-excursion if proof-sh= ell-exec-loop if if let proof-shell-filter-manage-output progn] 6 [save-e= xcursion let* pg-set-span-helphighlights proof-make-goalsave if let proof= -done-advancing-save cond let proof-done-advancing funcall condition-case= proof-shell-invoke-callback mapc let* save-excursion] 18 [proof-toolbar-= goto-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil= nil nil nil nil nil nil nil nil] 10 [if proof-make-goalsave if let proof= -done-advancing-save cond let proof-done-advancing funcall condition-case= proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec= -loop] 3 [proof-string-match if proof-string-match-safe and cond let proo= f-done-advancing funcall condition-case proof-shell-invoke-callback mapc = let* save-excursion if proof-shell-exec-loop if] 9 [coq-search-urgent-mes= sage setq and while let proof-shell-process-urgent-messages and save-excu= rsion proof-shell-filter progn condition-case while let if proof-shell-fi= lter-wrapper run-hook-with-args] 9 [if let save-current-buffer proof-shel= l-insert proof-shell-insert-action-item if let* save-excursion if proof-s= hell-exec-loop if if let proof-shell-filter-manage-output progn if] 9 [if= while let progn if let span-at-before prev-span setq while let proof-don= e-advancing-save cond let proof-done-advancing funcall] 8 [if coq-set-sta= te-infos run-hooks proof-done-advancing funcall condition-case proof-shel= l-invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if= let proof-shell-filter-manage-output] 7 [let company-coq-state-change ru= n-hooks proof-done-advancing funcall condition-case proof-shell-invoke-ca= llback mapc let* save-excursion if proof-shell-exec-loop if if let proof-= shell-filter-manage-output] 6 [condition-case while let if proof-shell-fi= lter-wrapper run-hook-with-args let save-current-buffer progn if let scom= int-output-filter nil nil nil nil] 1 [apply byte-code timer-event-handler= nil nil nil nil nil nil nil nil nil nil nil nil nil] 6 [cons if let if b= uild-list-id-from-string let progn if let coq-last-prompt-info coq-last-p= rompt-info-safe or let if coq-set-state-infos run-hooks] 16 [and or let c= ompany-coq-get-goals-window let if let company-coq-state-change run-hooks= proof-done-advancing funcall condition-case proof-shell-invoke-callback = mapc let* save-excursion] 10 [+ let* coq-module-opening-p or let or coq-g= oal-command-p funcall cond let proof-done-advancing-other cond let proof-= done-advancing funcall condition-case] 7 [goto-char let save-current-buff= er progn if let scomint-output-filter nil nil nil nil nil nil nil nil nil= ] 4 [and let* pg-remove-element "#" funcall "#<= lambda 0xa4306fd6cb>" mapc span-delete if while let proof-done-advancing-= save cond let proof-done-advancing funcall] 7 [span-delete mapc span-mapc= -spans span-delete-spans proof-script-delete-spans let if proof-done-retr= acting funcall condition-case proof-shell-invoke-callback mapc let* save-= excursion if proof-shell-exec-loop] 4 [file-name-sans-extension x-gtk-map= -stock redisplay_internal\ \(C\ function\) redisplay progn if let* proof-= shell-wait progn unwind-protect let if save-current-buffer let proof-prot= ected-process-or-retract if] 4 [replace-regexp-in-string progn if company= -coq--last-output-without-eager-annotation-markers company-coq-trim progn= unwind-protect let unwind-protect progn if progn if company-coq-ask-prov= er company-coq-unless-error company-coq-ask-prover-swallow-errors] 7 [if = while let* company-coq--split-seq mapcar let if let* if company-coq-tg--p= arse-group cons let cond let* if cond] 4 [last car concat company-coq-tg-= -mk-placeholder list list cond let cond let* company-coq-tg--format-tacti= c-rec let "#" funcall cond let*] 4 [while let*= let company-coq--list-to-table setq company-coq-tactic-initialize-notati= ons-filter progn if company-coq-prover-init run-hooks progn unwind-protec= t progn if let save-current-buffer] 4 [split-window-sensibly funcall wind= ow--try-to-split-window display-buffer-pop-up-window display-buffer--mayb= e-pop-up-frame-or-window display-buffer if if proof-get-window-for-buffer= let progn unwind-protect save-current-buffer let save-excursion if] 6 [p= g-add-element let proof-done-advancing-comment cond let proof-done-advanc= ing funcall condition-case proof-shell-invoke-callback mapc let progn if = let proof-add-to-queue proof-extend-queue] 6 [cond let proof-done-advanci= ng-other cond let proof-done-advancing funcall condition-case proof-shell= -invoke-callback mapc let* save-excursion if proof-shell-exec-loop if if]= 3 [let span-make-modifying-removing-span let* pg-set-span-helphighlights= let proof-done-advancing-other cond let proof-done-advancing funcall con= dition-case proof-shell-invoke-callback mapc let* save-excursion if] 3 [t= imer-event-handler nil nil nil nil nil nil nil nil nil nil nil nil nil ni= l nil] 4 [coq-set-span-proofstack if let if coq-set-state-infos run-hooks= proof-done-advancing funcall condition-case proof-shell-invoke-callback = mapc let* save-excursion if proof-shell-exec-loop if] 6 [while let if let= spans-at-point-prop car-safe span-at save-current-buffer proof-last-lock= ed-span if let if coq-set-state-infos run-hooks proof-done-advancing func= all] 3 [memq and let scomint-check-proc and proof-shell-live-buffer and p= roof-toolbar-find-enable-p redisplay_internal\ \(C\ function\) nil nil ni= l nil nil nil nil] 3 [time-add timer-relative-time timer-inc-time timer-e= vent-handler nil nil nil nil nil nil nil nil nil nil nil nil] 1 [and proo= f-re-search-forward-safe cond proof-shell-handle-immediate-output let pro= of-shell-filter-manage-output progn if let if if let save-excursion proof= -shell-filter progn condition-case] 26 [let scomint-check-proc and proof-= shell-live-buffer and proof-toolbar-find-enable-p redisplay_internal\ \(C= \ function\) nil nil nil nil nil nil nil nil nil] 10 [progn condition-cas= e while let if proof-shell-filter-wrapper run-hook-with-args let save-cur= rent-buffer progn if let scomint-output-filter nil nil nil] 3 [let if if = let save-excursion proof-shell-filter progn condition-case while let if p= roof-shell-filter-wrapper run-hook-with-args let save-current-buffer prog= n] 3 [let save-current-buffer proof-shell-insert proof-shell-insert-actio= n-item if let* save-excursion if proof-shell-exec-loop if if let proof-sh= ell-filter-manage-output progn if let] 15 [let proof-shell-filter-manage-= output progn if let if if let save-excursion proof-shell-filter progn con= dition-case while let if proof-shell-filter-wrapper] 9 [or let or coq-goa= l-command-p funcall cond let proof-done-advancing-other cond let proof-do= ne-advancing funcall condition-case proof-shell-invoke-callback mapc let*= ] 5 [while let proof-done-advancing-save cond let proof-done-advancing fu= ncall condition-case proof-shell-invoke-callback mapc let* save-excursion= if proof-shell-exec-loop if if] 6 [save-current-buffer proof-last-locked= -span if let if coq-set-state-infos run-hooks proof-done-advancing funcal= l condition-case proof-shell-invoke-callback mapc let* save-excursion if = proof-shell-exec-loop] 1 [span-set-property let span-make-modifying-remov= ing-span let* pg-set-span-helphighlights proof-make-goalsave if let proof= -done-advancing-save cond let proof-done-advancing funcall condition-case= proof-shell-invoke-callback mapc] 10 [let progn if let coq-last-prompt-i= nfo coq-last-prompt-info-safe or let if coq-set-state-infos run-hooks pro= of-done-retracting funcall condition-case proof-shell-invoke-callback map= c] 9 [let* progn unwind-protect save-current-buffer let company-coq-tg--p= reprocess-tactics-grammar let* company-coq-tg--extract-notations and let = company-coq-get-all-notations company-coq--list-to-table setq company-coq= -tactic-initialize-notations-filter progn if] 4 [company-coq-tg--parse-ta= ctic-part let cond let* if company-coq-tg--parse-tactic-part mapcar compa= ny-coq-tg--parse-tactic-subs cons company-coq-tg--parse-tactic mapcar let= if let* if company-coq-tg--parse-group] 4 [while let* reverse nconc setq= while let* condition-case let* company-coq-tg--extract-notations and let= company-coq-get-all-notations company-coq--list-to-table setq company-co= q-tactic-initialize-notations-filter] 4 [split-string last car concat com= pany-coq-tg--mk-placeholder list list cond let cond let* company-coq-tg--= format-tactic-rec let "#" funcall cond] 8 [nco= nc setq while let* let "#" funcall cond let* c= ond let* company-coq-tg--format-tactic-rec progn if company-coq-tg--forma= t-tactic let*] 4 [progn if coq-update-minor-mode-alist run-hooks let proo= f-shell-handle-delayed-output setq if if let proof-shell-filter-manage-ou= tput progn if let if if] 2 [redisplay_internal\ \(C\ function\) redisplay= progn if let* proof-shell-wait if progn if proof-shell-invisible-command= "#" mapcar if progn unwind-protect progn] 11 = [progn if let if let company-coq-state-change run-hooks proof-grab-lock p= rogn if progn if let proof-add-to-queue proof-start-queue let*] 5 [file-r= emote-p redisplay_internal\ \(C\ function\) message map-y-or-n-p save-som= e-buffers let coq-compile-save-some-buffers let progn if let while let le= t if coq-seq-preprocess-require-commands] 4 [let if coq-set-state-infos r= un-hooks proof-done-advancing funcall condition-case proof-shell-invoke-c= allback mapc let* save-excursion if proof-shell-exec-loop if if let] 4 [s= ave-excursion proof-locked-region-full-p not progn cond proof-toolbar-use= -enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil= nil nil] 3 [and company-coq-boundp-equal let* if company-coq-maybe-proof= -input-reload-things run-hooks let save-current-buffer proof-shell-insert= proof-shell-insert-action-item if let* save-excursion if proof-shell-exe= c-loop if] 9 [let* pg-remove-element "#" funcal= l "#" mapc span-delete if while let proof-done-advan= cing-save cond let proof-done-advancing funcall condition-case] 7 [and le= t* pg-remove-element "#" funcall "#" mapc span-delete if while let proof-done-advancing-save cond l= et proof-done-advancing funcall] 7 [span-property eq cond progn if while = let proof-done-advancing-save cond let proof-done-advancing funcall condi= tion-case proof-shell-invoke-callback mapc let*] 9 [internal--after-save-= selected-window unwind-protect save-current-buffer let save-excursion if = proof-display-and-keep-buffer pg-response-display if proof-shell-display-= output-as-response cond let proof-shell-handle-delayed-output setq if if]= 173 [redisplay sit-for progn unwind-protect let if save-current-buffer l= et proof-protected-process-or-retract if let* save-current-buffer if proo= f-deactivate-scripting progn condition-case] 1 [global-font-lock-mode-cmh= h kill-all-local-variables let progn scomint-mode if save-current-buffer = if scomint-make-in-buffer apply scomint-make apply let* let if proof-shel= l-start] 3 [eq cond let* cond let* company-coq-tg--format-tactic-rec prog= n if company-coq-tg--format-tactic let* reverse nconc setq while let* con= dition-case] 4 [coq-find-threeb-frames and if if coq-optimise-resp-window= s progn if coq-optimise-resp-windows-if-option run-hooks let proof-shell-= handle-delayed-output setq if if let proof-shell-filter-manage-output] 3 = [setq progn unwind-protect save-current-buffer let let coq-seq-get-librar= y-dependencies setq progn unwind-protect let coq-seq-map-module-id-to-obj= -file let coq-seq-check-module while let] 4 [proof-shell-insert-action-it= em if let* save-excursion if proof-shell-exec-loop if if let proof-shell-= filter-manage-output progn if let if if let] 11 [- span-at save-current-b= uffer proof-last-locked-span if let if coq-set-state-infos run-hooks proo= f-done-advancing funcall condition-case proof-shell-invoke-callback mapc = let* save-excursion] 4 [1+ if let proof-next-element-count proof-element-= id proof-next-element-id let proof-done-advancing-other cond let proof-do= ne-advancing funcall condition-case proof-shell-invoke-callback mapc let*= ] 2 [list eval redisplay_internal\ \(C\ function\) nil nil nil nil nil ni= l nil nil nil nil nil nil nil] 4 [coq-get-span-statenum or if let if coq-= set-state-infos run-hooks proof-done-advancing funcall condition-case pro= of-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-loo= p] 3 [save-excursion let* pg-set-span-helphighlights let let proof-done-a= dvancing-comment cond let proof-done-advancing funcall condition-case pro= of-shell-invoke-callback mapc let* save-excursion if] 4 [if pg-last-outpu= t-displayform let* pg-set-span-helphighlights let proof-done-advancing-ot= her cond let proof-done-advancing funcall condition-case proof-shell-invo= ke-callback mapc let* save-excursion if] 5 [and let scomint-check-proc an= d proof-shell-live-buffer and proof-toolbar-context-enable-p redisplay_in= ternal\ \(C\ function\) nil nil nil nil nil nil nil nil] 2 [while let coq= -search-urgent-message setq and while let proof-shell-process-urgent-mess= ages and save-excursion proof-shell-filter progn condition-case while let= if] 1 [proof-shell-live-buffer and proof-toolbar-context-enable-p redisp= lay_internal\ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil= nil] 8 [proof-string-match coq-section-command-p or let or coq-goal-comm= and-p funcall cond let proof-done-advancing-other cond let proof-done-adv= ancing funcall condition-case proof-shell-invoke-callback] 6 [memq and le= t scomint-check-proc and proof-shell-live-buffer and proof-toolbar-state-= enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil nil]= 3 [cond proof-toolbar-undo-enable-p redisplay_internal\ \(C\ function\) = nil nil nil nil nil nil nil nil nil nil nil nil nil] 3 [coq-last-prompt-i= nfo-safe or let if coq-set-state-infos run-hooks proof-done-advancing fun= call condition-case proof-shell-invoke-callback mapc let* save-excursion = if proof-shell-exec-loop if] 6 [proof-set-overlay-arrow proof-set-locked-= endpoints if proof-set-locked-end let proof-done-advancing funcall condit= ion-case proof-shell-invoke-callback mapc let* save-excursion if proof-sh= ell-exec-loop if if] 2 [proof-locked-region-full-p not progn cond proof-t= oolbar-use-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil n= il nil nil nil nil nil] 9 [proof-set-locked-end let proof-done-advancing = funcall condition-case proof-shell-invoke-callback mapc let* save-excursi= on if proof-shell-exec-loop if if let proof-shell-filter-manage-output pr= ogn] 5 [intern company-coq-feature-toggle-function let company-coq-featur= e-active-p or if company-coq--update-context let if company-coq-maybe-pro= of-output-reload-things run-hooks let proof-shell-handle-delayed-output s= etq if if] 3 [progn if let* proof-shell-wait catch progn if let* proof-sh= ell-kill-function kill-buffer let progn if if proof-shell-exit progn] 2 [= if let* company-coq-tg--find-tactics mapcar apply let cond let* if let* c= ompany-coq-tg--find-tactics mapcar apply let if let*] 4 [if eval redispla= y_internal\ \(C\ function\) redisplay progn if let* proof-shell-wait if p= rogn if proof-shell-invisible-command proof-shell-invisible-command-invis= ible-result mapc if progn] 2 [window--resize-reset-1 window--resize-reset= -1 window--resize-reset-1 window--resize-reset-1 window--resize-reset win= dow--resize-root-window-vertically message map-y-or-n-p save-some-buffers= let coq-compile-save-some-buffers let progn if let while] 3 [proof-strin= g-match and while let coq-count-match + let* coq-module-opening-p or let = or coq-goal-command-p funcall cond let proof-done-advancing-other] 5 [lis= t let* pg-add-element cond let proof-done-advancing-other cond let proof-= done-advancing funcall condition-case proof-shell-invoke-callback mapc le= t* save-excursion if] 7 [funcall redisplay--update-region-highlights appl= y "#" redisplay_internal\ \(C\ function\) nil nil nil = nil nil nil nil nil nil nil nil] 5 [proof-shell-live-buffer and proof-she= ll-available-p and progn cond proof-toolbar-undo-enable-p redisplay_inter= nal\ \(C\ function\) nil nil nil nil nil nil nil nil] 4 [and while let co= q-count-match let* coq-module-opening-p or let or coq-goal-command-p func= all cond progn if while let] 5 [scomint-check-proc and proof-shell-live-b= uffer and proof-toolbar-state-enable-p redisplay_internal\ \(C\ function\= ) nil nil nil nil nil nil nil nil nil nil] 6 [or or progn proof-shell-ins= ert proof-shell-insert-action-item if let* save-excursion if proof-shell-= exec-loop if if let proof-shell-filter-manage-output progn if] 8 [cond le= t proof-done-advancing funcall condition-case proof-shell-invoke-callback= mapc let* save-excursion if proof-shell-exec-loop if if let proof-shell-= filter-manage-output progn] 2 [let proof-string-match and let* coq-module= -opening-p or let or coq-goal-command-p funcall cond progn if while let p= roof-done-advancing-save] 9 [span-set-property let* pg-add-element cond l= et proof-done-advancing-other cond let proof-done-advancing funcall condi= tion-case proof-shell-invoke-callback mapc let* save-excursion if] 2 [map= c span-delete if while let proof-done-advancing-save cond let proof-done-= advancing funcall condition-case proof-shell-invoke-callback mapc let* sa= ve-excursion if] 2 [save-current-buffer let cond pg-response-display-with= -face let* proof-shell-process-urgent-message-default cond proof-shell-pr= ocess-urgent-message save-excursion if while let proof-shell-process-urge= nt-messages and save-excursion proof-shell-filter] 3 [x-gtk-map-stock red= isplay_internal\ \(C\ function\) redisplay progn if let* proof-shell-wait= progn unwind-protect let if save-current-buffer let proof-protected-proc= ess-or-retract if let*] 4 [if eval redisplay_internal\ \(C\ function\) re= display progn if let* proof-shell-wait progn unwind-protect let if save-c= urrent-buffer let proof-protected-process-or-retract if] 4 [company-coq-t= g--parse-tactic-part mapcar company-coq-tg--parse-tactic-subs cons compan= y-coq-tg--parse-tactic mapcar let if let* if company-coq-tg--parse-group = cons let cond let* if] 4 [reverse nconc setq while let* let "#" funcall cond let* cond let* company-coq-tg--format-tact= ic-rec let* let "#"] 76 [cond let* company-coq-= tg--format-tactic-rec let* let "#" funcall cond= let* cond let* company-coq-tg--format-tactic-rec let* let "#" funcall] 4 [version-to-list version< let coq--version< c= oq--pre-v85 coq-include-options nconc let coq-seq-get-library-dependencie= s setq progn unwind-protect let coq-seq-map-module-id-to-obj-file let coq= -seq-check-module] 4 [and proof-toolbar-state-enable-p redisplay_internal= \ \(C\ function\) nil nil nil nil nil nil nil nil nil nil nil nil nil] 4 = [save-excursion let* pg-set-span-helphighlights let pg-add-proof-element = let proof-make-goalsave if let proof-done-advancing-save cond let proof-d= one-advancing funcall condition-case proof-shell-invoke-callback] 6 [let = proof-string-match and while let coq-count-match let* coq-module-opening-= p or let or coq-goal-command-p funcall cond progn if] 2 [pg-set-span-help= highlights let proof-done-advancing-other cond let proof-done-advancing f= uncall condition-case proof-shell-invoke-callback mapc let* save-excursio= n if proof-shell-exec-loop if if] 5 [let scomint-send-input let save-curr= ent-buffer proof-shell-insert proof-shell-insert-action-item if let* save= -excursion if proof-shell-exec-loop if if let proof-shell-filter-manage-o= utput progn] 2 [and cond let proof-done-advancing funcall condition-case = proof-shell-invoke-callback mapc let* save-excursion if proof-shell-exec-= loop if if let proof-shell-filter-manage-output] 1 [not or if let proof-d= one-advancing funcall condition-case proof-shell-invoke-callback mapc let= * save-excursion if proof-shell-exec-loop if if let] 7 [proof-toolbar-ret= ract-enable-p redisplay_internal\ \(C\ function\) nil nil nil nil nil nil= nil nil nil nil nil nil nil nil] 174 [if let* save-excursion if proof-sh= ell-exec-loop if if let proof-shell-filter-manage-output progn if let if = if let save-excursion] 1 [profiler-cpu-profile profiler-report-cpu profil= er-report if if save-current-buffer pg-profile-1 apply byte-code timer-ev= ent-handler nil nil nil nil nil nil] 6 [Automatic\ GC] 593)) (22381 28814= 617335 579000) nil] --------------070201090105060902060102-- --8wjkfrrB5xTsuu5fvb2kRq81hVxxS2oTW-- --OQj6GK6Qj5dgbK1HBkts11r9kohkomv0V Content-Type: application/pgp-signature; name="signature.asc" Content-Description: OpenPGP digital signature Content-Disposition: attachment; filename="signature.asc" -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.22 (GNU/Linux) iQIcBAEBAgAGBQJXbXyPAAoJEPqg+cTm90wj8W0P+gJ8vBSIU6iehA5TaB7HUbQk BsgFwOqX2JfRt15WDac5k6+kQFAKraYjSkzQht1RhAiA8MXh0SCwhYpeseq32hMZ btAmVj2DdL4uXTGzSY6n2jqVr1pgdKfmq82th3MfQZnafpv9mXIEjHDilDvKG3oL /xH8L3rhG/nfqEJOuq7JVWAGxhcwit+Ok+A/FPBzSyMSbeuLsDLRG1nD34DWU2XG dwzvMhgmrXKMTLuQjC1ByoC0Wvg9fKApv88hOVlC0Wxvp2ju08Efj3wT/kMqgmx/ FT6f9TuV7GslOUvavBfox6obRdimgh6PbUw3vje4Yr8grYnjkcVO5d9DW7c+2m4j Gn4Yq6zF/MoG4zIJ0FWva91NkWmjADa+BZzPzfJUBBQyVdn+gGmbVIDgmQfd9GVb S55hgkoVk3kXKhvmIZ3UGBcFp1Kr/kkOSB6t7dRRNo2mgu7xhH88wdc2erTY+G8r CP8yenHJp73pkMd410zDC6AgM2GMt/u+Rgyk6Z5tcTmdO62GJz6qTAv1CHdTxY7/ qs3bGtRFbsOWDNBRdqtA/x0+dcuOB+i0qkaFcIkdQbFd42yHrsaYMMEwbjVVsMsv gbTNWXJ7Y311TEQlkzVOeBbnuFC5EKFyv1ss5wwMb0j3MtAfobsEhMtwc+46vu0s onivV7IzpFWarYKL51Ud =hzmF -----END PGP SIGNATURE----- --OQj6GK6Qj5dgbK1HBkts11r9kohkomv0V--