From 412e424b3305b12b753084328747233c3076dbbb Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Wed, 1 Apr 2020 17:48:33 -0400 Subject: Change "" into nil in argument to append --- coq/coq-system.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq/coq-system.el b/coq/coq-system.el index bc4c6b4f..e2a3431e 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -452,7 +452,7 @@ LOADPATH, CURRENT-DIRECTORY, PRE-V85: see `coq-coqc-prog-args'." (if (and topfile-supported buffer-file-name) (message "Warning: this Coq buffer is probably not compilable \ because of its name, no -topfile option set.")) - "") + nil) (cons "-emacs" (coq-coqc-prog-args loadpath current-directory pre-v85))))) (defun coq-prog-args () -- cgit v1.2.3 From a38887058166487607f03972d6d2c25ee9d5dada Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Wed, 1 Apr 2020 17:46:21 -0400 Subject: SearchAbout is deprecated since 8.5; use Search instead --- coq/coq-abbrev.el | 4 +--- coq/coq-syntax.el | 1 - coq/coq.el | 26 +++++++++----------------- coq/faq | 2 +- doc/ProofGeneral.texi | 2 +- 5 files changed, 12 insertions(+), 23 deletions(-) diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 391b1238..d1cb249d 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -261,10 +261,8 @@ ["About..." coq-About :help "With prefix arg (C-u): Set Printing All first"] ["About...(show implicits)" coq-About-with-implicits t] ["About...(show all)" coq-About-with-all t] - ["Search..." coq-SearchConstant t] + ["Search..." coq-Search t] ["SearchRewrite..." coq-SearchRewrite t] - ["SearchAbout (hiding principles)..." coq-SearchAbout t] - ["SearchAbout..." coq-SearchAbout-all t] ["SearchPattern..." coq-SearchIsos t] ["Locate constant..." coq-LocateConstant t] ["Locate Library..." coq-LocateLibrary t] diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 93db1a77..55a12117 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -563,7 +563,6 @@ so for the following reasons: ("Print" "p" "Print #." nil "Print") ("Pwd" nil "Pwd." nil "Pwd") ("Search" nil "Search #" nil "Search") - ("SearchAbout" nil "SearchAbout #" nil "SearchAbout") ("SearchPattern" nil "SearchPattern (#)" nil "SearchPattern") ("SearchRewrite" nil "SearchRewrite #" nil "SearchRewrite") ("Show" nil "Show #." nil "Show") diff --git a/coq/coq.el b/coq/coq.el index 8acc1b72..0c934a9b 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1005,17 +1005,10 @@ This is specific to `coq-mode'." "SearchPattern (parenthesis mandatory), ex: (?X1 + _ = _ + ?X1)" "SearchPattern" nil)) -(defun coq-SearchConstant () - (interactive) - (coq-ask-do "Search constant" "Search")) - (defun coq-SearchRewrite () (interactive) (coq-ask-do "SearchRewrite" "SearchRewrite" nil)) - - - (defun coq-Print (withprintingall) "Ask for an ident and print the corresponding term. With flag Printing All if some prefix arg is given (C-u)." @@ -1487,7 +1480,7 @@ fold/unfold cross. Return the list of mappings hypname -> overlays." ;; Feature: highlighting of hypothesis that remains when the script is played ;; (and goals buffer is updated). -;; On by default. This only works with the SearchAbout function for now. +;; On by default. This only works with the Search function for now. (defvar coq-highlight-hyps-cited-in-response t "If non-nil, try to highlight in goals buffers hyps cited in response.") @@ -1559,7 +1552,7 @@ of hypothesis to highlight." (defun coq-get-hyps-cited-in-response () "Returns locations of hyps in goals buffer that are cited in response buffer. -See `coq-highlight-hyps-cited-in-response' and `SearchAbout'." +See `coq-highlight-hyps-cited-in-response' and `Search'." (let* ((hyps-cited-pos (coq-detect-hyps-positions proof-response-buffer)) (hyps-cited (coq-build-hyps-names hyps-cited-pos))) (cl-remove-if-not @@ -2678,15 +2671,13 @@ Completion is on a quasi-exhaustive list of Coq tacticals." "Set Printing All" q "Unset Printing All" nil "Test Printing All") (proof-shell-invisible-command q)))) - -;; TODO SearchAbout become Search in v8.5, change when V8.4 becomes old. -(defun coq-SearchAbout () +(defun coq-Search () (interactive) (coq-ask-do ;; TODO: use [Add Search Blacklist "foo"] to exclude optionaly some patterns: ;; "_ind" "_rec" "R_" "_equation" - "SearchAbout (ex: \"eq_\" eq -bool)" - "SearchAbout" + "Search (ex: \"eq_\" eq -bool)" + "Search" nil nil t) (when coq-highlight-hyps-cited-in-response (coq-highlight-hyps-cited-in-response) @@ -2694,6 +2685,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (unless coq-highlight-hyps-cited-in-response (message "[Coq/Settings/Search Blacklist] to change blacklisting."))) + ;; Insertion commands (define-key coq-keymap [(control ?i)] 'coq-insert-intros) (define-key coq-keymap [(control ?m)] 'coq-insert-match) @@ -2717,7 +2709,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-keymap [(control ?o)] 'coq-SearchIsos) (define-key coq-keymap [(control ?p)] 'coq-Print) (define-key coq-keymap [(control ?b)] 'coq-About) -(define-key coq-keymap [(control ?a)] 'coq-SearchAbout) +(define-key coq-keymap [(control ?a)] 'coq-Search) (define-key coq-keymap [(control ?c)] 'coq-Check) (define-key coq-keymap [?h] 'coq-PrintHint) (define-key coq-keymap [(control ?l)] 'coq-LocateConstant) @@ -2734,7 +2726,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?p)] 'coq-Print) (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?o)] 'coq-SearchIsos) (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?b)] 'coq-About) -(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?a)] 'coq-SearchAbout) +(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?a)] 'coq-Search) (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?s)] 'coq-Show) (define-key coq-goals-mode-map [(control ?c)(control ?a)?r] 'proof-store-response-win) (define-key coq-goals-mode-map [(control ?c)(control ?a)?g] 'proof-store-goals-win) @@ -2754,7 +2746,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?p)] 'coq-Print) (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?o)] 'coq-SearchIsos) (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?b)] 'coq-About) -(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?a)] 'coq-SearchAbout) +(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?a)] 'coq-Search) (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?s)] 'coq-Show) (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?r)] 'proof-store-response-win) (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?g)] 'proof-store-goals-win) diff --git a/coq/faq b/coq/faq index 40873850..8b2cb06f 100644 --- a/coq/faq +++ b/coq/faq @@ -113,7 +113,7 @@ printing options temporarily disable (Set Printing All). *** C-c C-a C-p The same for a ``Print '' query. *** C-c C-a C-b The same for a ``About '' query. -*** C-c C-a C-a The same for a ``SearchAbout '' query (no C-u prefix). +*** C-c C-a C-a The same for a ``Search '' query (no C-u prefix). *** C-c C-a C-o The same for a Search ``SearchIsos'' (no C-u prefix). ** I hate menus, why do you have menus? diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 23aba63b..699b304b 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4342,7 +4342,7 @@ The same for a ``Print '' query. @item C-c C-a C-b The same for a ``About '' query. @item C-c C-a C-a -The same for a ``SearchAbout '' query (no C-u prefix). +The same for a ``Search '' query (no C-u prefix). @item C-c C-a C-o The same for a Search ``SearchIsos'' (no C-u prefix). -- cgit v1.2.3 From e4e34b98fde31d813ac583f806fc3b95e3cf6059 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Mon, 30 Mar 2020 09:00:26 -0500 Subject: Add support for core Ltac2 syntax - Ltac2 definitions, types, and notation - Ltac2 queries - ltac1:(...) and ltac2:(...) antiquotations Closes #473. --- coq/coq-syntax.el | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 93db1a77..3f52a998 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -488,8 +488,12 @@ so for the following reasons: ("Instance" nil "Instance #:#.\nProof.\n#Defined." t "Instance") ("Program Instance" "pinstance" "Program Instance [ # ] => # where \n# := #;\n# := #." t "Program\\s-+Instance") ("Let" "Let" "Let # : # := #." t "Let") - ("Local Ltac" nil "Local Ltac # := #" t "Local\\s-+Ltac") - ("Ltac" "ltac" "Ltac # := #" t "Ltac") + ("Local Ltac2" nil "Local Ltac2 # := #." t "Local\\s-+Ltac2") + ("Ltac2 Type" "lt2ty" "Ltac2 Type # := #." t "Ltac2 Type") + ("Ltac2 Type" "lt2oty" "Ltac2 Type # ::= #." t "Ltac2 Type") + ("Ltac2" "lt2" "Ltac2 # := #." t "Ltac2") + ("Local Ltac" nil "Local Ltac # := #." t "Local\\s-+Ltac") + ("Ltac" "ltac" "Ltac # := #." t "Ltac") ("Module :=" "mo" "Module # : # := #." t ) ; careful ("Module <: :=" "mo2" "Module # <: # := #." t ) ; careful ("Module Import :=" "moi" "Module Import # : # := #." t ) ; careful @@ -560,6 +564,7 @@ so for the following reasons: ("Locate" nil "Locate" nil "Locate") ("Print Coercions" nil "Print Coercions." nil "Print\\s-+Coercions") ("Print Hint" nil "Print Hint." nil "Print\\s-+Hint" coq-PrintHint) + ("Print Ltac2" "lt2p" "Print Ltac2 #." nil "Print Ltac2") ("Print" "p" "Print #." nil "Print") ("Pwd" nil "Pwd." nil "Pwd") ("Search" nil "Search #" nil "Search") @@ -626,6 +631,8 @@ so for the following reasons: ("Import" nil "Import #." t "Import") ("Include" nil "Include #." t "Include") ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix") + ("Ltac2 Notation" "lt2n" "Ltac2 Notation # := #." t "Ltac2 Notation") + ("Ltac2 Eval" "lt2e" "Ltac2 Eval #." nil "Ltac2 Eval") ("Notation (assoc)" "notas" "Notation \"#\" := # (at level #, # associativity)." t) ("Notation (at assoc)" "notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." t) ("Notation (at at scope)" "notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." t) @@ -1335,7 +1342,7 @@ It is used: (defconst coq-context-marker-regexp - (concat (regexp-opt '("ltac" "constr" "uconstr") 'symbols) ":")) + (concat (regexp-opt '("ltac" "constr" "uconstr" "ltac1" "ltac2") 'symbols) ":")) ;; ;; font-lock -- cgit v1.2.3 From a03dc31801972cbcff38035a30711da34d66ed78 Mon Sep 17 00:00:00 2001 From: Lawrence Dunn Date: Thu, 2 Apr 2020 12:56:27 -0400 Subject: Correct documentation --- doc/ProofGeneral.texi | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 699b304b..5f1e8231 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -924,8 +924,7 @@ example in Isabelle with semi-colons, but these will not appear in the final text. Coq, on the other hand, requires a full-stop terminator at the end of -each line, so @kbd{C-c .} is the key binding used to turn on -electric terminator. If you don't know what the terminator character +each line. If you don't know what the terminator character is, you can find the option anyway on the menu: @code{Proof-General -> Quick Options -> Processing -> Electric Terminator} which also shows the key binding. -- cgit v1.2.3 From 1f56706ff2f0870a461ded0f5a40292df8bcd96a Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Thu, 2 Apr 2020 20:20:00 +0200 Subject: Rephrase ProofGeneral.texi following PR #476 that fixed #475 Note that currently, there is no keybinding associated to the electric terminator. --- doc/ProofGeneral.texi | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 5f1e8231..c2cb3be5 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -924,17 +924,15 @@ example in Isabelle with semi-colons, but these will not appear in the final text. Coq, on the other hand, requires a full-stop terminator at the end of -each line. If you don't know what the terminator character -is, you can find the option anyway on the menu: +each line. If you want to enable electric terminator, use the menu item: @code{Proof-General -> Quick Options -> Processing -> Electric Terminator} -which also shows the key binding. - -If you want to use electric terminator, you can customize Proof -General to enable it every time if you want, @xref{Customizing Proof -General}. For the common options, customization is easy: just -use the menu item @code{Proof General -> Quick Options} to make your choices, -and @code{Proof-General -> Quick Options -> Save Options} to -save your choices. + +If you want to keep electric terminator enabled all the time, you can +customize Proof General to do so, @xref{Customizing Proof General}. For +the common options, customization is easy: just use the menu item +@code{Proof General -> Quick Options} to make your choices, and +@code{Proof-General -> Quick Options -> Save Options} to save your +choices. -- cgit v1.2.3