Update

1 files changed, 534 insertions, 527 deletions

diff --git a/TAGS b/TAGS
index 9a2265d9..f9af9b08 100644
--- a/TAGS
+++ b/TAGS
@@ -16,8 +16,8 @@ coq/coq-abbrev.el,495
 (defconst coq-terms-menu46,1296
 (defconst coq-terms-abbrev-table51,1434
 (defun coq-install-abbrevs 58,1628
-(defpgdefault menu-entries83,2604
-(defpgdefault help-menu-entries148,4718
+(defpgdefault menu-entries80,2533
+(defpgdefault help-menu-entries145,4647
 
 coq/coq-db.el,678
 (defconst coq-syntax-db 24,596
@@ -31,14 +31,14 @@ coq/coq-db.el,678
 (defun coq-build-menu-from-db 190,6988
 (defcustom coq-holes-minor-mode 212,7827
 (defun coq-build-abbrev-table-from-db 218,7971
-(defun filter-state-preserving 237,8609
-(defun filter-state-changing 242,8763
-(defface coq-solve-tactics-face249,8984
-(defface coq-cheat-face258,9314
-(defconst coq-solve-tactics-face 266,9562
-(defconst coq-cheat-face 270,9726
-
-coq/coq.el,7728
+(defun filter-state-preserving 237,8597
+(defun filter-state-changing 242,8751
+(defface coq-solve-tactics-face249,8972
+(defface coq-cheat-face258,9302
+(defconst coq-solve-tactics-face 266,9550
+(defconst coq-cheat-face 270,9714
+
+coq/coq.el,8039
 (defcustom coq-translate-to-v8 60,1872
 (defun coq-build-prog-args 66,2051
 (defcustom coq-compiler76,2345
@@ -46,250 +46,257 @@ coq/coq.el,7728
 (defcustom coq-use-makefile 88,2622
 (defcustom coq-default-undo-limit 96,2844
 (defconst coq-shell-init-cmd101,2972
-(defcustom coq-prog-env 109,3237
-(defconst coq-shell-restart-cmd 117,3486
-(defvar coq-shell-prompt-pattern119,3540
-(defvar coq-shell-cd 127,3843
-(defvar coq-shell-proof-completed-regexp 131,4003
-(defvar coq-goal-regexp134,4158
-(defun get-coq-library-directory 139,4254
-(defconst coq-library-directory 145,4436
-(defcustom coq-tags 148,4562
-(defconst coq-interrupt-regexp 153,4710
-(defcustom coq-www-home-page 156,4803
-(defvar coq-outline-regexp167,4978
-(defvar coq-outline-heading-end-regexp 174,5190
-(defvar coq-shell-outline-regexp 176,5244
-(defvar coq-shell-outline-heading-end-regexp 177,5294
-(defconst coq-state-preserving-tactics-regexp180,5358
-(defconst coq-state-changing-commands-regexp182,5460
-(defconst coq-state-preserving-commands-regexp184,5569
-(defconst coq-commands-regexp186,5682
-(defvar coq-retractable-instruct-regexp188,5761
-(defvar coq-non-retractable-instruct-regexp190,5853
-(defcustom coq-use-smie 222,6549
-(defconst coq-smie-grammar230,6777
-(defun coq-smie-rules 268,8598
-(defun coq-set-undo-limit 291,9329
-(defun build-list-id-from-string 295,9459
-(defun coq-last-prompt-info 307,9957
-(defun coq-last-prompt-info-safe 319,10489
-(defvar coq-last-but-one-statenum 325,10746
-(defvar coq-last-but-one-proofnum 332,11043
-(defvar coq-last-but-one-proofstack 335,11141
-(defsubst coq-get-span-statenum 338,11251
-(defsubst coq-get-span-proofnum 342,11366
-(defsubst coq-get-span-proofstack 346,11481
-(defsubst coq-set-span-statenum 350,11625
-(defsubst coq-get-span-goalcmd 354,11756
-(defsubst coq-set-span-goalcmd 358,11870
-(defsubst coq-set-span-proofnum 362,12000
-(defsubst coq-set-span-proofstack 366,12131
-(defsubst proof-last-locked-span 370,12291
-(defun proof-clone-buffer 374,12425
-(defun proof-store-buffer-win 388,12960
-(defun proof-store-response-win 399,13453
-(defun proof-store-goals-win 403,13580
-(defun coq-set-state-infos 415,14112
-(defun count-not-intersection 453,16198
-(defun coq-find-and-forget 483,17450
-(defvar coq-current-goal 510,18755
-(defun coq-goal-hyp 513,18820
-(defun coq-state-preserving-p 526,19294
-(defconst notation-print-kinds-table540,19608
-(defun coq-PrintScope 544,19775
-(defun coq-guess-or-ask-for-string 562,20324
-(defun coq-ask-do 576,20864
-(defsubst coq-put-into-brackets 585,21249
-(defsubst coq-put-into-quotes 588,21310
-(defun coq-SearchIsos 591,21369
-(defun coq-SearchConstant 599,21608
-(defun coq-Searchregexp 603,21701
-(defun coq-SearchRewrite 609,21842
-(defun coq-SearchAbout 613,21939
-(defun coq-Print 619,22082
-(defun coq-About 624,22206
-(defun coq-LocateConstant 629,22325
-(defun coq-LocateLibrary 634,22428
-(defun coq-LocateNotation 639,22545
-(defun coq-Pwd 647,22776
-(defun coq-Inspect 652,22900
-(defun coq-PrintSection(656,23000
-(defun coq-Print-implicit 660,23093
-(defun coq-Check 665,23244
-(defun coq-Show 670,23352
-(defun coq-Compile 684,23795
-(defun coq-guess-command-line 696,24113
-(defpacustom use-editing-holes 733,25666
-(defun coq-mode-config 742,25969
-(defun coq-shell-mode-config 836,29296
-(defun coq-goals-mode-config 881,31124
-(defun coq-response-config 888,31368
-(defpacustom print-fully-explicit 913,32193
-(defpacustom print-implicit 918,32341
-(defpacustom print-coercions 923,32507
-(defpacustom print-match-wildcards 928,32651
-(defpacustom print-elim-types 933,32831
-(defpacustom printing-depth 938,32997
-(defpacustom undo-depth 943,33158
-(defpacustom time-commands 948,33324
-(defgroup coq-auto-compile 981,34683
-(defpacustom compile-before-require 986,34834
-(defcustom coq-compile-command 998,35326
-(defpacustom confirm-external-compilation 1028,36609
-(defconst coq-compile-substitution-list1037,36916
-(defcustom coq-compile-auto-save 1057,37837
-(defcustom coq-lock-ancestors 1082,38895
-(defcustom coq-compile-ignore-library-directory 1091,39216
-(defcustom coq-compile-ignored-directories 1103,39704
-(defcustom coq-load-path 1116,40337
-(defcustom coq-load-path-include-current 1131,40893
-(defconst coq-require-command-regexp1140,41211
-(defconst coq-require-id-regexp1147,41568
-(defvar coq-compile-history 1155,42002
-(defvar coq-compile-response-buffer-name 1158,42086
-(defvar coq-compile-response-buffer 1161,42225
-(defvar coq-debug-auto-compilation 1165,42327
-(defun time-less-or-equal 1171,42434
-(defun coq-max-dep-mod-time 1179,42772
-(defun coq-prog-args 1202,43576
-(defun coq-lock-ancestor 1211,43835
-(defun coq-unlock-ancestor 1227,44610
-(defun coq-unlock-all-ancestors-of-span 1234,44905
-(defun coq-compile-ignore-file 1241,45201
-(defun coq-library-src-of-obj-file 1265,46084
-(defun coq-include-options 1270,46316
-(defun coq-init-compile-response-buffer 1289,47089
-(defun coq-display-compile-response-buffer 1311,48156
-(defun coq-get-library-dependencies 1325,48777
-(defun coq-compile-library 1372,51004
-(defun coq-compile-library-if-necessary 1399,52209
-(defun coq-make-lib-up-to-date 1445,54081
-(defun coq-auto-compile-externally 1501,56542
-(defun coq-map-module-id-to-obj-file 1544,58688
-(defun coq-check-module 1596,61219
-(defvar coq-process-require-current-buffer1624,62661
-(defun coq-compile-save-buffer-filter 1630,62926
-(defun coq-compile-save-some-buffers 1640,63340
-(defun coq-preprocess-require-commands 1662,64242
-(defun coq-switch-buffer-kill-proof-shell 1695,65811
-(defun coq-preprocessing 1715,66487
-(defun coq-fake-constant-markup 1729,66942
-(defun coq-create-span-menu 1745,67547
-(defconst module-kinds-table1763,68060
-(defconst modtype-kinds-table1767,68209
-(defun coq-insert-section-or-module 1771,68338
-(defconst reqkinds-kinds-table1792,69188
-(defun coq-insert-requires 1796,69332
-(defun coq-end-Section 1809,69811
-(defun coq-insert-intros 1827,70389
-(defun coq-insert-infoH-hook 1839,70920
-(defun coq-insert-as 1844,71128
-(defun coq-insert-match 1861,71818
-(defun coq-insert-solve-tactic 1890,72987
-(defun coq-insert-tactic 1896,73238
-(defun coq-insert-tactical 1902,73440
-(defun coq-insert-command 1908,73671
-(defun coq-insert-term 1913,73836
-(define-key coq-keymap 1918,73997
-(define-key coq-keymap 1919,74055
-(define-key coq-keymap 1920,74112
-(define-key coq-keymap 1921,74181
-(define-key coq-keymap 1922,74237
-(define-key coq-keymap 1923,74286
-(define-key coq-keymap 1924,74344
-(define-key coq-keymap 1925,74404
-(define-key coq-keymap 1926,74469
-(define-key coq-keymap 1929,74597
-(define-key coq-keymap 1931,74671
-(define-key coq-keymap 1932,74728
-(define-key coq-keymap 1936,74853
-(define-key coq-keymap 1938,74909
-(define-key coq-keymap 1939,74959
-(define-key coq-keymap 1940,75009
-(define-key coq-keymap 1941,75065
-(define-key coq-keymap 1942,75115
-(define-key coq-keymap 1943,75169
-(define-key coq-keymap 1944,75228
-(define-key coq-goals-mode-map 1947,75289
-(define-key coq-goals-mode-map 1948,75371
-(define-key coq-goals-mode-map 1949,75453
-(define-key coq-goals-mode-map 1950,75540
-(define-key coq-goals-mode-map 1951,75622
-(defvar last-coq-error-location 1960,75924
-(defun coq-get-last-error-location 1968,76308
-(defun coq-highlight-error 2018,78871
-(defun coq-highlight-error-hook 2046,79952
-(defun first-word-of-buffer 2056,80169
-(defun coq-show-first-goal 2064,80372
-(defvar coq-modeline-string2 2080,81037
-(defvar coq-modeline-string1 2081,81071
-(defvar coq-modeline-string0 2082,81105
-(defun coq-build-subgoals-string 2083,81146
-(defun coq-update-minor-mode-alist 2088,81312
-(defun is-not-split-vertic 2120,82705
-(defun optim-resp-windows 2129,83145
-
-coq/coq-indent.el,2515
+(defcustom coq-prog-env 109,3248
+(defconst coq-shell-restart-cmd 117,3497
+(defvar coq-shell-prompt-pattern119,3551
+(defvar coq-shell-cd 127,3854
+(defvar coq-shell-proof-completed-regexp 131,4014
+(defvar coq-goal-regexp134,4169
+(defun get-coq-library-directory 139,4265
+(defconst coq-library-directory 145,4447
+(defcustom coq-tags 148,4573
+(defconst coq-interrupt-regexp 153,4721
+(defcustom coq-www-home-page 156,4814
+(defvar coq-outline-regexp167,4989
+(defvar coq-outline-heading-end-regexp 174,5201
+(defvar coq-shell-outline-regexp 176,5255
+(defvar coq-shell-outline-heading-end-regexp 177,5305
+(defconst coq-state-preserving-tactics-regexp180,5369
+(defconst coq-state-changing-commands-regexp182,5471
+(defconst coq-state-preserving-commands-regexp184,5580
+(defconst coq-commands-regexp186,5693
+(defvar coq-retractable-instruct-regexp188,5772
+(defvar coq-non-retractable-instruct-regexp190,5864
+(defcustom coq-use-smie 222,6560
+(defconst coq-smie-grammar230,6788
+(defun coq-smie-search-token-forward 286,9346
+(defun coq-smie-search-token-backward 299,9853
+(defun coq-smie-forward-token 325,11065
+(defun coq-smie-backward-token 362,12510
+(defun coq-smie-rules 401,13979
+(defconst coq-script-command-end-regexp 468,16882
+(defun coq-empty-command-p 473,17010
+(defun coq-script-parse-function 488,17729
+(defun coq-set-undo-limit 495,17955
+(defun build-list-id-from-string 499,18085
+(defun coq-last-prompt-info 511,18583
+(defun coq-last-prompt-info-safe 523,19115
+(defvar coq-last-but-one-statenum 529,19372
+(defvar coq-last-but-one-proofnum 536,19669
+(defvar coq-last-but-one-proofstack 539,19767
+(defsubst coq-get-span-statenum 542,19877
+(defsubst coq-get-span-proofnum 546,19992
+(defsubst coq-get-span-proofstack 550,20107
+(defsubst coq-set-span-statenum 554,20251
+(defsubst coq-get-span-goalcmd 558,20382
+(defsubst coq-set-span-goalcmd 562,20496
+(defsubst coq-set-span-proofnum 566,20626
+(defsubst coq-set-span-proofstack 570,20757
+(defsubst proof-last-locked-span 574,20917
+(defun proof-clone-buffer 578,21051
+(defun proof-store-buffer-win 592,21586
+(defun proof-store-response-win 603,22079
+(defun proof-store-goals-win 607,22206
+(defun coq-set-state-infos 619,22738
+(defun count-not-intersection 657,24824
+(defun coq-find-and-forget 687,26076
+(defvar coq-current-goal 714,27381
+(defun coq-goal-hyp 717,27446
+(defun coq-state-preserving-p 730,27920
+(defconst notation-print-kinds-table744,28234
+(defun coq-PrintScope 748,28401
+(defun coq-guess-or-ask-for-string 766,28950
+(defun coq-ask-do 780,29490
+(defsubst coq-put-into-brackets 789,29875
+(defsubst coq-put-into-quotes 792,29936
+(defun coq-SearchIsos 795,29995
+(defun coq-SearchConstant 803,30234
+(defun coq-Searchregexp 807,30327
+(defun coq-SearchRewrite 813,30468
+(defun coq-SearchAbout 817,30565
+(defun coq-Print 823,30708
+(defun coq-About 828,30832
+(defun coq-LocateConstant 833,30951
+(defun coq-LocateLibrary 838,31054
+(defun coq-LocateNotation 843,31171
+(defun coq-Pwd 851,31402
+(defun coq-Inspect 856,31526
+(defun coq-PrintSection(860,31626
+(defun coq-Print-implicit 864,31719
+(defun coq-Check 869,31870
+(defun coq-Show 874,31978
+(defun coq-Compile 888,32421
+(defun coq-guess-command-line 900,32739
+(defpacustom use-editing-holes 937,34292
+(defun coq-mode-config 946,34595
+(defun coq-shell-mode-config 1042,38075
+(defun coq-goals-mode-config 1087,39903
+(defun coq-response-config 1094,40147
+(defpacustom print-fully-explicit 1119,40972
+(defpacustom print-implicit 1124,41120
+(defpacustom print-coercions 1129,41286
+(defpacustom print-match-wildcards 1134,41430
+(defpacustom print-elim-types 1139,41610
+(defpacustom printing-depth 1144,41776
+(defpacustom undo-depth 1149,41937
+(defpacustom time-commands 1154,42103
+(defgroup coq-auto-compile 1165,42353
+(defpacustom compile-before-require 1170,42504
+(defcustom coq-compile-command 1182,42996
+(defpacustom confirm-external-compilation 1212,44279
+(defconst coq-compile-substitution-list1221,44586
+(defcustom coq-compile-auto-save 1241,45507
+(defcustom coq-lock-ancestors 1266,46565
+(defcustom coq-compile-ignore-library-directory 1275,46886
+(defcustom coq-compile-ignored-directories 1287,47374
+(defcustom coq-load-path 1300,48007
+(defcustom coq-load-path-include-current 1315,48563
+(defconst coq-require-command-regexp1324,48881
+(defconst coq-require-id-regexp1331,49238
+(defvar coq-compile-history 1339,49672
+(defvar coq-compile-response-buffer 1342,49756
+(defvar coq-debug-auto-compilation 1346,49891
+(defun time-less-or-equal 1352,49999
+(defun coq-max-dep-mod-time 1360,50337
+(defun coq-prog-args 1383,51141
+(defun coq-lock-ancestor 1392,51400
+(defun coq-unlock-ancestor 1408,52175
+(defun coq-unlock-all-ancestors-of-span 1415,52470
+(defun coq-compile-ignore-file 1422,52766
+(defun coq-library-src-of-obj-file 1446,53649
+(defun coq-include-options 1451,53881
+(defun coq-init-compile-response-buffer 1470,54654
+(defun coq-display-compile-response-buffer 1493,55726
+(defun coq-get-library-dependencies 1507,56360
+(defun coq-compile-library 1554,58586
+(defun coq-compile-library-if-necessary 1581,59797
+(defun coq-make-lib-up-to-date 1627,61669
+(defun coq-auto-compile-externally 1683,64130
+(defun coq-map-module-id-to-obj-file 1726,66276
+(defun coq-check-module 1779,68878
+(defvar coq-process-require-current-buffer1807,70320
+(defun coq-compile-save-buffer-filter 1813,70585
+(defun coq-compile-save-some-buffers 1823,70999
+(defun coq-preprocess-require-commands 1845,71901
+(defun coq-switch-buffer-kill-proof-shell 1878,73470
+(defun coq-preprocessing 1898,74146
+(defun coq-fake-constant-markup 1912,74601
+(defun coq-create-span-menu 1928,75206
+(defconst module-kinds-table1946,75719
+(defconst modtype-kinds-table1950,75868
+(defun coq-insert-section-or-module 1954,75997
+(defconst reqkinds-kinds-table1975,76847
+(defun coq-insert-requires 1979,76991
+(defun coq-end-Section 1992,77470
+(defun coq-insert-intros 2010,78048
+(defun coq-insert-infoH-hook 2022,78579
+(defun coq-insert-as 2027,78787
+(defun coq-insert-match 2044,79480
+(defun coq-insert-solve-tactic 2073,80649
+(defun coq-insert-tactic 2079,80900
+(defun coq-insert-tactical 2085,81102
+(defun coq-insert-command 2091,81333
+(defun coq-insert-term 2096,81498
+(define-key coq-keymap 2101,81659
+(define-key coq-keymap 2102,81717
+(define-key coq-keymap 2103,81774
+(define-key coq-keymap 2104,81843
+(define-key coq-keymap 2105,81899
+(define-key coq-keymap 2106,81948
+(define-key coq-keymap 2107,82006
+(define-key coq-keymap 2108,82056
+(define-key coq-keymap 2109,82111
+(define-key coq-keymap 2111,82164
+(define-key coq-keymap 2113,82238
+(define-key coq-keymap 2114,82295
+(define-key coq-keymap 2117,82360
+(define-key coq-keymap 2118,82420
+(define-key coq-keymap 2120,82476
+(define-key coq-keymap 2121,82526
+(define-key coq-keymap 2122,82576
+(define-key coq-keymap 2123,82632
+(define-key coq-keymap 2124,82682
+(define-key coq-keymap 2125,82726
+(define-key coq-keymap 2126,82785
+(define-key coq-goals-mode-map 2129,82846
+(define-key coq-goals-mode-map 2130,82928
+(define-key coq-goals-mode-map 2131,83010
+(define-key coq-goals-mode-map 2132,83097
+(define-key coq-goals-mode-map 2133,83179
+(defvar last-coq-error-location 2142,83481
+(defun coq-get-last-error-location 2150,83865
+(defun coq-highlight-error 2200,86428
+(defun coq-highlight-error-hook 2228,87509
+(defun first-word-of-buffer 2238,87726
+(defun coq-show-first-goal 2246,87929
+(defvar coq-modeline-string2 2262,88594
+(defvar coq-modeline-string1 2263,88628
+(defvar coq-modeline-string0 2264,88662
+(defun coq-build-subgoals-string 2265,88703
+(defun coq-update-minor-mode-alist 2270,88869
+(defun is-not-split-vertic 2302,90262
+(defun optim-resp-windows 2311,90702
+
+coq/coq-indent.el,2527
 (defconst coq-any-command-regexp20,368
 (defconst coq-indent-inner-regexp23,442
-(defconst coq-comment-start-regexp 33,796
-(defconst coq-comment-end-regexp 34,839
-(defconst coq-comment-start-or-end-regexp35,880
-(defconst coq-indent-open-regexp37,988
-(defconst coq-indent-close-regexp42,1164
-(defconst coq-indent-closepar-regexp 45,1275
-(defconst coq-indent-closematch-regexp 46,1320
-(defconst coq-indent-openpar-regexp 47,1391
-(defconst coq-indent-openmatch-regexp 48,1435
-(defconst coq-tacticals-tactics-regex49,1515
-(defconst coq-indent-any-regexp51,1634
-(defconst coq-indent-kw55,1850
-(defconst coq-indent-pattern-regexp 65,2316
-(defun coq-indent-goal-command-p 69,2419
-(defconst coq-end-command-regexp91,3470
-(defun coq-search-comment-delimiter-forward 96,3622
-(defun coq-search-comment-delimiter-backward 105,3952
-(defun coq-skip-until-one-comment-backward 112,4226
-(defun coq-skip-until-one-comment-forward 127,4933
-(defun coq-looking-at-comment 138,5451
-(defun coq-find-comment-start 142,5592
-(defun coq-find-comment-end 153,6025
-(defun coq-looking-at-syntactic-context 165,6518
-(defconst coq-end-command-or-comment-regexp171,6740
-(defconst coq-end-command-or-comment-start-regexp174,6849
-(defun coq-find-not-in-comment-backward 178,6967
-(defun coq-find-not-in-comment-forward 198,7868
-(defun coq-find-command-end-backward 222,9007
-(defun coq-find-command-end-forward 231,9398
-(defun coq-find-command-end 240,9775
-(defun coq-find-current-start 248,10107
-(defun coq-find-real-start 257,10398
-(defun coq-command-at-point 264,10617
-(defun same-line 272,10903
-(defun coq-commands-at-line 275,10990
-(defun coq-indent-only-spaces-on-line 294,11613
-(defun coq-indent-find-reg 300,11890
-(defun coq-find-no-syntactic-on-line 314,12426
-(defun coq-back-to-indentation-prevline 327,12899
-(defun coq-find-unclosed 370,14785
-(defun coq-find-at-same-level-zero 400,16095
-(defun coq-find-unopened 429,17361
-(defun coq-find-last-unopened 472,18795
-(defun coq-end-offset 483,19192
-(defun coq-add-iter 508,19962
-(defun coq-goal-count 511,20068
-(defun coq-save-count 513,20140
-(defun coq-proof-count 515,20226
-(defun coq-goal-save-diff-maybe-proof 519,20401
-(defun coq-indent-command-offset 526,20622
-(defun coq-indent-expr-offset 558,22225
-(defun coq-indent-comment-offset 673,26909
-(defun coq-indent-offset 705,28358
-(defun coq-indent-calculate 724,29233
-(defun coq-indent-line 727,29321
-(defun coq-indent-line-not-comments 737,29687
-(defun coq-indent-region 747,30076
+(defconst coq-comment-start-regexp 33,804
+(defconst coq-comment-end-regexp 34,847
+(defconst coq-comment-start-or-end-regexp35,888
+(defconst coq-indent-open-regexp37,996
+(defconst coq-indent-close-regexp42,1193
+(defconst coq-indent-closepar-regexp 48,1392
+(defconst coq-indent-closematch-regexp 49,1437
+(defconst coq-indent-openpar-regexp 50,1508
+(defconst coq-indent-openmatch-regexp 51,1552
+(defconst coq-tacticals-tactics-regex52,1632
+(defconst coq-indent-any-regexp54,1751
+(defconst coq-indent-kw58,1967
+(defconst coq-indent-pattern-regexp 68,2433
+(defun coq-indent-goal-command-p 72,2536
+(defconst coq-end-command-regexp94,3590
+(defun coq-search-comment-delimiter-forward 102,3996
+(defun coq-search-comment-delimiter-backward 111,4326
+(defun coq-skip-until-one-comment-backward 118,4600
+(defun coq-skip-until-one-comment-forward 133,5307
+(defun coq-looking-at-comment 144,5825
+(defun coq-find-comment-start 148,5966
+(defun coq-find-comment-end 159,6399
+(defun coq-looking-at-syntactic-context 171,6892
+(defconst coq-end-command-or-comment-regexp177,7114
+(defconst coq-end-command-or-comment-start-regexp180,7223
+(defun coq-find-not-in-comment-backward 183,7340
+(defun coq-find-not-in-comment-forward 203,8230
+(defun coq-is-on-ending-context 228,9404
+(defun coq-script-parse-cmdend-forward 241,9916
+(defun coq-script-parse-cmdend-backward 281,11778
+(defun coq-find-current-start 317,13275
+(defun coq-find-real-start 326,13601
+(defun same-line 332,13819
+(defun coq-command-at-point 335,13906
+(defun coq-commands-at-line 349,14501
+(defun coq-indent-only-spaces-on-line 373,15466
+(defun coq-indent-find-reg 379,15743
+(defun coq-find-no-syntactic-on-line 393,16279
+(defun coq-back-to-indentation-prevline 406,16752
+(defun coq-find-unclosed 452,18819
+(defun coq-find-at-same-level-zero 482,20129
+(defun coq-find-unopened 511,21395
+(defun coq-find-last-unopened 554,22829
+(defun coq-end-offset 565,23226
+(defun coq-add-iter 590,23996
+(defun coq-goal-count 593,24102
+(defun coq-save-count 595,24174
+(defun coq-proof-count 600,24376
+(defun coq-goal-save-diff-maybe-proof 606,24664
+(defun coq-indent-command-offset 616,24958
+(defun coq-indent-expr-offset 682,28139
+(defun coq-indent-comment-offset 801,33021
+(defun coq-indent-offset 833,34473
+(defun coq-indent-calculate 852,35347
+(defun coq-indent-line 855,35435
+(defun coq-indent-line-not-comments 865,35801
+(defun coq-indent-region 875,36190
 
 coq/coq-local-vars.el,229
 (defconst coq-local-vars-doc 20,431
@@ -299,7 +306,7 @@ coq/coq-local-vars.el,229
 (defun coq-ask-prog-name 131,4952
 (defun coq-ask-insert-coq-prog-name 148,5663
 
-coq/coq-syntax.el,2768
+coq/coq-syntax.el,2771
 (defcustom coq-prog-name 18,560
 (defcustom coq-user-tactics-db 33,1148
 (defcustom coq-user-commands-db 50,1661
@@ -308,67 +315,67 @@ coq/coq-syntax.el,2768
 (defcustom coq-user-cheat-tactics-db 98,3220
 (defcustom coq-user-reserved-db 117,3766
 (defvar coq-tactics-db135,4297
-(defvar coq-solve-tactics-db293,12556
-(defvar coq-solve-cheat-tactics-db316,13401
-(defvar coq-tacticals-db328,13576
-(defvar coq-decl-db352,14462
-(defvar coq-defn-db377,15918
-(defvar coq-goal-starters-db435,20273
-(defvar coq-other-commands-db464,22030
-(defvar coq-commands-db593,31496
-(defvar coq-terms-db600,31716
-(defun coq-count-match 662,34331
-(defun coq-module-opening-p 678,35060
-(defun coq-section-command-p 689,35471
-(defun coq-goal-command-str-p 693,35568
-(defun coq-goal-command-p 720,36670
-(defvar coq-keywords-save-strict729,36953
-(defvar coq-keywords-save738,37066
-(defun coq-save-command-p 742,37144
-(defvar coq-keywords-kill-goal753,37472
-(defvar coq-keywords-state-changing-misc-commands757,37562
-(defvar coq-keywords-goal760,37687
-(defvar coq-keywords-decl763,37770
-(defvar coq-keywords-defn766,37844
-(defvar coq-keywords-state-changing-commands770,37919
-(defvar coq-keywords-state-preserving-commands779,38179
-(defvar coq-keywords-commands784,38395
-(defvar coq-solve-tactics789,38543
-(defvar coq-solve-tactics-regexp793,38664
-(defvar coq-solve-cheat-tactics797,38798
-(defvar coq-solve-cheat-tactics-regexp801,38943
-(defvar coq-tacticals805,39101
-(defvar coq-reserved811,39240
-(defvar coq-reserved-regexp 821,39567
-(defvar coq-state-changing-tactics823,39632
-(defvar coq-state-preserving-tactics826,39741
-(defvar coq-tactics830,39855
-(defvar coq-tactics-regexp 833,39944
-(defvar coq-retractable-instruct836,40099
-(defvar coq-non-retractable-instruct839,40209
-(defvar coq-keywords843,40337
-(defun proof-regexp-alt-list-symb 849,40561
-(defvar coq-keywords-regexp 852,40666
-(defvar coq-symbols855,40734
-(defvar coq-error-regexp 874,40947
-(defvar coq-id 877,41175
-(defvar coq-id-shy 878,41200
-(defvar coq-ids 881,41302
-(defun coq-first-abstr-regexp 883,41368
-(defcustom coq-variable-highlight-enable 886,41463
-(defvar coq-font-lock-terms892,41590
-(defconst coq-save-command-regexp-strict914,42673
-(defconst coq-save-command-regexp920,42843
-(defconst coq-save-with-hole-regexp925,42998
-(defconst coq-goal-command-regexp929,43158
-(defconst coq-goal-with-hole-regexp932,43260
-(defconst coq-decl-with-hole-regexp936,43394
-(defconst coq-defn-with-hole-regexp943,43644
-(defconst coq-with-with-hole-regexp953,43934
-(defvar coq-font-lock-keywords-1968,44464
-(defvar coq-font-lock-keywords 996,45799
-(defun coq-init-syntax-table 998,45857
-(defconst coq-generic-expression1023,46584
+(defvar coq-solve-tactics-db308,13431
+(defvar coq-solve-cheat-tactics-db335,14454
+(defvar coq-tacticals-db347,14629
+(defvar coq-decl-db371,15515
+(defvar coq-defn-db396,16971
+(defvar coq-goal-starters-db461,21693
+(defvar coq-other-commands-db490,23425
+(defvar coq-commands-db624,33366
+(defvar coq-terms-db631,33586
+(defun coq-count-match 693,36201
+(defun coq-module-opening-p 709,36930
+(defun coq-section-command-p 720,37341
+(defun coq-goal-command-str-p 724,37438
+(defun coq-goal-command-p 751,38540
+(defvar coq-keywords-save-strict761,38879
+(defvar coq-keywords-save768,39120
+(defun coq-save-command-p 773,39199
+(defvar coq-keywords-kill-goal784,39527
+(defvar coq-keywords-state-changing-misc-commands788,39617
+(defvar coq-keywords-goal791,39742
+(defvar coq-keywords-decl794,39825
+(defvar coq-keywords-defn797,39899
+(defvar coq-keywords-state-changing-commands801,39974
+(defvar coq-keywords-state-preserving-commands810,40234
+(defvar coq-keywords-commands815,40450
+(defvar coq-solve-tactics820,40598
+(defvar coq-solve-tactics-regexp824,40719
+(defvar coq-solve-cheat-tactics828,40853
+(defvar coq-solve-cheat-tactics-regexp832,40998
+(defvar coq-tacticals836,41156
+(defvar coq-reserved842,41295
+(defvar coq-reserved-regexp 852,41630
+(defvar coq-state-changing-tactics856,41741
+(defvar coq-state-preserving-tactics859,41850
+(defvar coq-tactics863,41964
+(defvar coq-tactics-regexp 866,42053
+(defvar coq-retractable-instruct869,42208
+(defvar coq-non-retractable-instruct872,42318
+(defvar coq-keywords876,42446
+(defun proof-regexp-alt-list-symb 882,42670
+(defvar coq-keywords-regexp 885,42775
+(defvar coq-symbols888,42848
+(defvar coq-error-regexp 910,43089
+(defvar coq-id 913,43317
+(defvar coq-id-shy 914,43342
+(defvar coq-ids 917,43444
+(defun coq-first-abstr-regexp 919,43510
+(defcustom coq-variable-highlight-enable 922,43605
+(defvar coq-font-lock-terms928,43732
+(defconst coq-save-command-regexp-strict950,44815
+(defconst coq-save-command-regexp956,44983
+(defconst coq-save-with-hole-regexp961,45136
+(defconst coq-goal-command-regexp965,45296
+(defconst coq-goal-with-hole-regexp968,45398
+(defconst coq-decl-with-hole-regexp972,45532
+(defconst coq-defn-with-hole-regexp979,45782
+(defconst coq-with-with-hole-regexp989,46072
+(defvar coq-font-lock-keywords-11004,46602
+(defvar coq-font-lock-keywords 1032,47937
+(defun coq-init-syntax-table 1034,47995
+(defconst coq-generic-expression1059,48722
 
 coq/coq-unicode-tokens.el,454
 (defconst coq-token-format 39,1427
@@ -1085,92 +1092,92 @@ generic/pg-response.el,1252
 (defun pg-thms-buffer-clear 481,16161
 
 generic/pg-user.el,3635
-(defun proof-script-new-command-advance 42,1231
-(defun proof-maybe-follow-locked-end 66,2156
-(defun proof-goto-command-start 92,2992
-(defun proof-goto-command-end 115,3939
-(defun proof-forward-command 130,4361
-(defun proof-backward-command 151,5082
-(defun proof-goto-point 162,5296
-(defun proof-assert-next-command-interactive 176,5730
-(defun proof-assert-until-point-interactive 188,6216
-(defun proof-process-buffer 194,6446
-(defun proof-undo-last-successful-command 212,6958
-(defun proof-undo-and-delete-last-successful-command 217,7120
-(defun proof-undo-last-successful-command-1 229,7641
-(defun proof-retract-buffer 246,8305
-(defun proof-retract-current-goal 255,8589
-(defun proof-mouse-goto-point 274,9109
-(defvar proof-minibuffer-history 289,9385
-(defun proof-minibuffer-cmd 292,9480
-(defun proof-frob-locked-end 331,10887
-(defmacro proof-if-setting-configured 367,11988
-(defmacro proof-define-assistant-command 375,12257
-(defmacro proof-define-assistant-command-witharg 388,12712
-(defun proof-issue-new-command 408,13534
-(defun proof-cd-sync 448,14757
-(defun proof-electric-terminator-enable 499,16356
-(defun proof-electric-terminator 507,16660
-(defun proof-add-completions 531,17440
-(defun proof-script-complete 554,18263
-(defun pg-copy-span-contents 568,18572
-(defun pg-numth-span-higher-or-lower 582,18996
-(defun pg-control-span-of 608,19742
-(defun pg-move-span-contents 614,19946
-(defun pg-fixup-children-spans 665,22064
-(defun pg-move-region-down 675,22321
-(defun pg-move-region-up 684,22614
-(defun pg-pos-for-event 698,22888
-(defun pg-span-for-event 704,23109
-(defun pg-span-context-menu 708,23253
-(defun pg-toggle-visibility 724,23770
-(defun pg-create-in-span-context-menu 733,24077
-(defun pg-span-undo 758,25105
-(defun pg-goals-buffers-hint 771,25343
-(defun pg-slow-fontify-tracing-hint 775,25561
-(defun pg-response-buffers-hint 779,25750
-(defun pg-jump-to-end-hint 791,26165
-(defun pg-processing-complete-hint 795,26294
-(defun pg-next-error-hint 812,27014
-(defun pg-hint 817,27166
-(defun pg-identifier-under-mouse-query 828,27515
-(defun pg-identifier-near-point-query 839,27839
-(defvar proof-query-identifier-history 868,28762
-(defun proof-query-identifier 871,28849
-(defun pg-identifier-query 882,29205
-(defun proof-imenu-enable 915,30353
-(defvar pg-input-ring 951,31656
-(defvar pg-input-ring-index 954,31713
-(defvar pg-stored-incomplete-input 957,31785
-(defun pg-previous-input 960,31888
-(defun pg-next-input 974,32351
-(defun pg-delete-input 979,32473
-(defun pg-get-old-input 992,32811
-(defun pg-restore-input 1006,33202
-(defun pg-search-start 1017,33492
-(defun pg-regexp-arg 1029,33984
-(defun pg-search-arg 1041,34432
-(defun pg-previous-matching-input-string-position 1055,34849
-(defun pg-previous-matching-input 1082,36014
-(defun pg-next-matching-input 1101,36864
-(defvar pg-matching-input-from-input-string 1109,37247
-(defun pg-previous-matching-input-from-input 1113,37361
-(defun pg-next-matching-input-from-input 1131,38126
-(defun pg-add-to-input-history 1142,38505
-(defun pg-remove-from-input-history 1154,38958
-(defun  pg-clear-input-ring 1165,39338
-(define-key proof-mode-map 1182,39808
-(define-key proof-mode-map 1183,39868
-(defun pg-protected-undo 1185,39940
-(defun pg-protected-undo-1 1215,41234
-(defun next-undo-elt 1246,42671
-(defvar proof-autosend-timer 1273,43627
-(deflocal proof-autosend-modified-tick 1275,43688
-(defun proof-autosend-enable 1279,43810
-(defun proof-autosend-delay 1293,44353
-(defun proof-autosend-loop 1297,44486
-(defun proof-autosend-loop-all 1311,45046
-(defun proof-autosend-loop-next 1335,45826
+(defun proof-script-new-command-advance 43,1232
+(defun proof-maybe-follow-locked-end 67,2157
+(defun proof-goto-command-start 93,2993
+(defun proof-goto-command-end 116,3940
+(defun proof-forward-command 131,4362
+(defun proof-backward-command 152,5083
+(defun proof-goto-point 163,5297
+(defun proof-assert-next-command-interactive 177,5731
+(defun proof-assert-until-point-interactive 189,6217
+(defun proof-process-buffer 195,6447
+(defun proof-undo-last-successful-command 213,6959
+(defun proof-undo-and-delete-last-successful-command 218,7121
+(defun proof-undo-last-successful-command-1 230,7640
+(defun proof-retract-buffer 247,8304
+(defun proof-retract-current-goal 256,8588
+(defun proof-mouse-goto-point 275,9108
+(defvar proof-minibuffer-history 290,9384
+(defun proof-minibuffer-cmd 293,9479
+(defun proof-frob-locked-end 332,10886
+(defmacro proof-if-setting-configured 368,11987
+(defmacro proof-define-assistant-command 376,12256
+(defmacro proof-define-assistant-command-witharg 389,12711
+(defun proof-issue-new-command 409,13533
+(defun proof-cd-sync 449,14756
+(defun proof-electric-terminator-enable 500,16355
+(defun proof-electric-terminator 508,16659
+(defun proof-add-completions 532,17439
+(defun proof-script-complete 555,18262
+(defun pg-copy-span-contents 569,18571
+(defun pg-numth-span-higher-or-lower 583,18995
+(defun pg-control-span-of 609,19741
+(defun pg-move-span-contents 615,19945
+(defun pg-fixup-children-spans 666,22063
+(defun pg-move-region-down 676,22320
+(defun pg-move-region-up 685,22613
+(defun pg-pos-for-event 699,22887
+(defun pg-span-for-event 705,23108
+(defun pg-span-context-menu 709,23252
+(defun pg-toggle-visibility 725,23769
+(defun pg-create-in-span-context-menu 734,24076
+(defun pg-span-undo 759,25104
+(defun pg-goals-buffers-hint 772,25342
+(defun pg-slow-fontify-tracing-hint 776,25560
+(defun pg-response-buffers-hint 780,25749
+(defun pg-jump-to-end-hint 792,26164
+(defun pg-processing-complete-hint 796,26293
+(defun pg-next-error-hint 813,27013
+(defun pg-hint 818,27165
+(defun pg-identifier-under-mouse-query 829,27514
+(defun pg-identifier-near-point-query 840,27838
+(defvar proof-query-identifier-history 869,28761
+(defun proof-query-identifier 872,28848
+(defun pg-identifier-query 883,29204
+(defun proof-imenu-enable 916,30352
+(defvar pg-input-ring 952,31655
+(defvar pg-input-ring-index 955,31712
+(defvar pg-stored-incomplete-input 958,31784
+(defun pg-previous-input 961,31887
+(defun pg-next-input 975,32350
+(defun pg-delete-input 980,32472
+(defun pg-get-old-input 993,32810
+(defun pg-restore-input 1007,33201
+(defun pg-search-start 1018,33491
+(defun pg-regexp-arg 1030,33983
+(defun pg-search-arg 1042,34431
+(defun pg-previous-matching-input-string-position 1056,34848
+(defun pg-previous-matching-input 1083,36013
+(defun pg-next-matching-input 1102,36863
+(defvar pg-matching-input-from-input-string 1110,37246
+(defun pg-previous-matching-input-from-input 1114,37360
+(defun pg-next-matching-input-from-input 1132,38125
+(defun pg-add-to-input-history 1143,38504
+(defun pg-remove-from-input-history 1155,38957
+(defun  pg-clear-input-ring 1166,39337
+(define-key proof-mode-map 1183,39807
+(define-key proof-mode-map 1184,39867
+(defun pg-protected-undo 1186,39939
+(defun pg-protected-undo-1 1216,41233
+(defun next-undo-elt 1247,42670
+(defvar proof-autosend-timer 1274,43626
+(deflocal proof-autosend-modified-tick 1276,43687
+(defun proof-autosend-enable 1280,43809
+(defun proof-autosend-delay 1294,44352
+(defun proof-autosend-loop 1298,44485
+(defun proof-autosend-loop-all 1312,45045
+(defun proof-autosend-loop-next 1336,45825
 
 generic/pg-vars.el,1500
 (defvar proof-assistant-cusgrp 22,388
@@ -1244,8 +1251,8 @@ generic/pg-xml.el,1177
 (defun pg-pgip-get-pgmltext 222,7237
 
 generic/proof-autoloads.el,97
-(defsubst proof-shell-live-buffer 716,23229
-(defsubst proof-replace-regexp-in-string 869,28708
+(defsubst proof-shell-live-buffer 722,23445
+(defsubst proof-replace-regexp-in-string 875,28925
 
 generic/proof-auxmodes.el,149
 (defun proof-mmm-support-available 20,495
@@ -1550,131 +1557,131 @@ generic/proof-mmm.el,70
 (defun proof-mmm-enable 58,1978
 
 generic/proof-script.el,5813
-(deflocal proof-active-buffer-fake-minor-mode 46,1414
-(deflocal proof-script-buffer-file-name 49,1540
-(deflocal pg-script-portions 56,1950
-(defalias 'proof-active-buffer-fake-minor-modeproof-active-buffer-fake-minor-mode
59,2056
-(defun proof-next-element-count 68,2251
-(defun proof-element-id 74,2493
-(defun proof-next-element-id 78,2662
-(deflocal proof-locked-span 114,3966
-(deflocal proof-queue-span 121,4232
-(deflocal proof-overlay-arrow 130,4718
-(defun proof-span-give-warning 136,4845
-(defun proof-span-read-only 142,5025
-(defun proof-strict-read-only 151,5398
-(defsubst proof-set-queue-endpoints 161,5776
-(defun proof-set-overlay-arrow 165,5917
-(defsubst proof-set-locked-endpoints 176,6255
-(defsubst proof-detach-queue 181,6431
-(defsubst proof-detach-locked 186,6570
-(defsubst proof-set-queue-start 193,6795
-(defsubst proof-set-locked-end 197,6921
-(defsubst proof-set-queue-end 209,7391
-(defun proof-init-segmentation 220,7688
-(defun proof-colour-locked 250,8939
-(defun proof-colour-locked-span 257,9212
-(defun proof-sticky-errors 263,9485
-(defun proof-restart-buffers 276,9901
-(defun proof-script-buffers-with-spans 300,10834
-(defun proof-script-remove-all-spans-and-deactivate 310,11190
-(defun proof-script-clear-queue-spans-on-error 314,11380
-(defun proof-script-delete-spans 340,12397
-(defun proof-script-delete-secondary-spans 345,12596
-(defun proof-unprocessed-begin 358,12885
-(defun proof-script-end 366,13139
-(defun proof-queue-or-locked-end 375,13449
-(defun proof-locked-region-full-p 394,14042
-(defun proof-locked-region-empty-p 403,14314
-(defun proof-only-whitespace-to-locked-region-p 407,14464
-(defun proof-in-locked-region-p 417,14813
-(defun proof-goto-end-of-locked 429,15070
-(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 446,15829
-(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 457,16310
-(defun proof-end-of-locked-visible-p 469,16850
-(defconst pg-idioms 488,17443
-(defconst pg-all-idioms 491,17539
-(defun pg-clear-script-portions 495,17660
-(defun pg-remove-element 501,17895
-(defun pg-get-element 509,18198
-(defun pg-add-element 519,18513
-(defun pg-invisible-prop 567,20475
-(defun pg-set-element-span-invisible 572,20676
-(defun pg-toggle-element-span-visibility 585,21242
-(defun pg-open-invisible-span 590,21403
-(defun pg-make-element-invisible 595,21574
-(defun pg-make-element-visible 600,21785
-(defun pg-toggle-element-visibility 605,21979
-(defun pg-show-all-portions 611,22242
-(defun pg-show-all-proofs 633,22986
-(defun pg-hide-all-proofs 638,23114
-(defun pg-add-proof-element 643,23245
-(defun pg-span-name 658,24032
-(defvar pg-span-context-menu-keymap691,25239
-(defun pg-last-output-displayform 698,25477
-(defun pg-set-span-helphighlights 721,26368
-(defun proof-complete-buffer-atomic 784,28515
-(defun proof-register-possibly-new-processed-file813,29785
-(defun proof-query-save-this-buffer-p 859,31659
-(defun proof-inform-prover-file-retracted 864,31884
-(defun proof-auto-retract-dependencies 884,32735
-(defun proof-unregister-buffer-file-name 938,35285
-(defsubst proof-action-completed 984,37110
-(defun proof-protected-process-or-retract 988,37280
-(defun proof-deactivate-scripting-auto 1016,38511
-(defun proof-deactivate-scripting-query-user-action 1025,38869
-(defun proof-deactivate-scripting-choose-action 1069,40378
-(defun proof-deactivate-scripting 1081,40763
-(defun proof-activate-scripting 1178,44886
-(defun proof-toggle-active-scripting 1278,49411
-(defun proof-done-advancing 1317,50656
-(defun proof-done-advancing-comment 1385,53153
-(defun proof-done-advancing-save 1419,54539
-(defun proof-make-goalsave1507,57903
-(defun proof-get-name-from-goal 1525,58768
-(defun proof-done-advancing-autosave 1545,59793
-(defun proof-done-advancing-other 1609,62289
-(defun proof-segment-up-to-parser 1638,63253
-(defun proof-script-generic-parse-find-comment-end 1707,65519
-(defun proof-script-generic-parse-cmdend 1716,65933
-(defun proof-script-generic-parse-cmdstart 1767,67829
-(defun proof-script-generic-parse-sexp 1806,69429
-(defun proof-semis-to-vanillas 1818,69895
-(defun proof-next-command-new-line 1871,71568
-(defun proof-script-next-command-advance 1876,71774
-(defun proof-assert-until-point 1895,72274
-(defun proof-assert-electric-terminator 1911,72945
-(defun proof-assert-semis 1955,74625
-(defun proof-retract-before-change 1969,75386
-(defun proof-insert-pbp-command 1989,75982
-(defun proof-insert-sendback-command 2004,76485
-(defun proof-done-retracting 2030,77388
-(defun proof-setup-retract-action 2065,78842
-(defun proof-last-goal-or-goalsave 2077,79447
-(defun proof-retract-target 2101,80359
-(defun proof-retract-until-point-interactive 2180,83612
-(defun proof-retract-until-point 2189,84019
-(define-derived-mode proof-mode 2244,86027
-(defun proof-script-set-visited-file-name 2280,87409
-(defun proof-script-set-buffer-hooks 2302,88422
-(defun proof-script-kill-buffer-fn 2310,88840
-(defun proof-config-done-related 2342,90157
-(defun proof-generic-goal-command-p 2407,92642
-(defun proof-generic-state-preserving-p 2412,92855
-(defun proof-generic-count-undos 2421,93372
-(defun proof-generic-find-and-forget 2452,94500
-(defconst proof-script-important-settings2503,96272
-(defun proof-config-done 2518,96818
-(defun proof-setup-parsing-mechanism 2585,98983
-(defun proof-setup-imenu 2609,100055
-(deflocal proof-segment-up-to-cache 2646,101337
-(deflocal proof-segment-up-to-cache-start 2650,101480
-(deflocal proof-segment-up-to-cache-end 2651,101525
-(deflocal proof-last-edited-low-watermark 2652,101568
-(defun proof-segment-up-to-using-cache 2654,101616
-(defun proof-segment-cache-contents-for 2682,102734
-(defun proof-script-after-change-function 2699,103316
-(defun proof-script-set-after-change-functions 2711,103823
+(deflocal proof-active-buffer-fake-minor-mode 46,1416
+(deflocal proof-script-buffer-file-name 49,1542
+(deflocal pg-script-portions 56,1952
+(defalias 'proof-active-buffer-fake-minor-modeproof-active-buffer-fake-minor-mode
59,2058
+(defun proof-next-element-count 68,2253
+(defun proof-element-id 74,2495
+(defun proof-next-element-id 78,2664
+(deflocal proof-locked-span 114,3968
+(deflocal proof-queue-span 121,4234
+(deflocal proof-overlay-arrow 130,4720
+(defun proof-span-give-warning 136,4847
+(defun proof-span-read-only 142,5027
+(defun proof-strict-read-only 151,5400
+(defsubst proof-set-queue-endpoints 161,5778
+(defun proof-set-overlay-arrow 165,5919
+(defsubst proof-set-locked-endpoints 176,6257
+(defsubst proof-detach-queue 181,6433
+(defsubst proof-detach-locked 186,6572
+(defsubst proof-set-queue-start 193,6797
+(defsubst proof-set-locked-end 197,6923
+(defsubst proof-set-queue-end 209,7393
+(defun proof-init-segmentation 220,7690
+(defun proof-colour-locked 250,8941
+(defun proof-colour-locked-span 257,9214
+(defun proof-sticky-errors 263,9487
+(defun proof-restart-buffers 276,9903
+(defun proof-script-buffers-with-spans 300,10836
+(defun proof-script-remove-all-spans-and-deactivate 310,11192
+(defun proof-script-clear-queue-spans-on-error 314,11382
+(defun proof-script-delete-spans 340,12399
+(defun proof-script-delete-secondary-spans 345,12598
+(defun proof-unprocessed-begin 358,12887
+(defun proof-script-end 366,13141
+(defun proof-queue-or-locked-end 375,13451
+(defun proof-locked-region-full-p 394,14044
+(defun proof-locked-region-empty-p 403,14316
+(defun proof-only-whitespace-to-locked-region-p 407,14466
+(defun proof-in-locked-region-p 417,14815
+(defun proof-goto-end-of-locked 429,15072
+(defun proof-goto-end-of-locked-if-pos-not-visible-in-window 446,15831
+(defun proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window 457,16312
+(defun proof-end-of-locked-visible-p 469,16852
+(defconst pg-idioms 488,17445
+(defconst pg-all-idioms 491,17541
+(defun pg-clear-script-portions 495,17662
+(defun pg-remove-element 501,17897
+(defun pg-get-element 509,18200
+(defun pg-add-element 519,18515
+(defun pg-invisible-prop 567,20477
+(defun pg-set-element-span-invisible 572,20678
+(defun pg-toggle-element-span-visibility 585,21244
+(defun pg-open-invisible-span 590,21405
+(defun pg-make-element-invisible 595,21576
+(defun pg-make-element-visible 600,21787
+(defun pg-toggle-element-visibility 605,21981
+(defun pg-show-all-portions 611,22244
+(defun pg-show-all-proofs 633,22988
+(defun pg-hide-all-proofs 638,23116
+(defun pg-add-proof-element 643,23247
+(defun pg-span-name 658,24034
+(defvar pg-span-context-menu-keymap691,25241
+(defun pg-last-output-displayform 698,25479
+(defun pg-set-span-helphighlights 721,26370
+(defun proof-complete-buffer-atomic 784,28517
+(defun proof-register-possibly-new-processed-file813,29787
+(defun proof-query-save-this-buffer-p 859,31661
+(defun proof-inform-prover-file-retracted 864,31886
+(defun proof-auto-retract-dependencies 884,32737
+(defun proof-unregister-buffer-file-name 938,35287
+(defsubst proof-action-completed 984,37112
+(defun proof-protected-process-or-retract 988,37282
+(defun proof-deactivate-scripting-auto 1016,38513
+(defun proof-deactivate-scripting-query-user-action 1025,38871
+(defun proof-deactivate-scripting-choose-action 1069,40380
+(defun proof-deactivate-scripting 1081,40765
+(defun proof-activate-scripting 1178,44888
+(defun proof-toggle-active-scripting 1278,49413
+(defun proof-done-advancing 1317,50658
+(defun proof-done-advancing-comment 1385,53155
+(defun proof-done-advancing-save 1419,54541
+(defun proof-make-goalsave1507,57905
+(defun proof-get-name-from-goal 1525,58770
+(defun proof-done-advancing-autosave 1545,59795
+(defun proof-done-advancing-other 1609,62291
+(defun proof-segment-up-to-parser 1638,63255
+(defun proof-script-generic-parse-find-comment-end 1708,65536
+(defun proof-script-generic-parse-cmdend 1717,65950
+(defun proof-script-generic-parse-cmdstart 1768,67846
+(defun proof-script-generic-parse-sexp 1807,69446
+(defun proof-semis-to-vanillas 1819,69912
+(defun proof-next-command-new-line 1872,71585
+(defun proof-script-next-command-advance 1877,71791
+(defun proof-assert-until-point 1896,72291
+(defun proof-assert-electric-terminator 1912,72962
+(defun proof-assert-semis 1956,74642
+(defun proof-retract-before-change 1970,75403
+(defun proof-insert-pbp-command 1993,76059
+(defun proof-insert-sendback-command 2008,76562
+(defun proof-done-retracting 2034,77465
+(defun proof-setup-retract-action 2069,78919
+(defun proof-last-goal-or-goalsave 2081,79524
+(defun proof-retract-target 2105,80436
+(defun proof-retract-until-point-interactive 2184,83689
+(defun proof-retract-until-point 2193,84096
+(define-derived-mode proof-mode 2248,86101
+(defun proof-script-set-visited-file-name 2284,87483
+(defun proof-script-set-buffer-hooks 2306,88496
+(defun proof-script-kill-buffer-fn 2314,88914
+(defun proof-config-done-related 2346,90231
+(defun proof-generic-goal-command-p 2411,92716
+(defun proof-generic-state-preserving-p 2416,92929
+(defun proof-generic-count-undos 2425,93446
+(defun proof-generic-find-and-forget 2456,94574
+(defconst proof-script-important-settings2507,96346
+(defun proof-config-done 2522,96892
+(defun proof-setup-parsing-mechanism 2589,99057
+(defun proof-setup-imenu 2613,100129
+(deflocal proof-segment-up-to-cache 2650,101411
+(deflocal proof-segment-up-to-cache-start 2654,101554
+(deflocal proof-segment-up-to-cache-end 2655,101599
+(deflocal proof-last-edited-low-watermark 2656,101642
+(defun proof-segment-up-to-using-cache 2658,101690
+(defun proof-segment-cache-contents-for 2686,102810
+(defun proof-script-after-change-function 2703,103392
+(defun proof-script-set-after-change-functions 2715,103899
 
 generic/proof-shell.el,3653
 (defvar proof-marker 34,746