Merge branch 'master' of https://github.com/ProofGeneral/PG

6 files changed, 30 insertions, 37 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 0eb707f7..8db7781e 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -277,10 +277,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..1722f1bc 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,10 +564,10 @@ 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")
-     ("SearchAbout" nil "SearchAbout #" nil "SearchAbout")
      ("SearchPattern" nil "SearchPattern (#)" nil "SearchPattern")
      ("SearchRewrite" nil "SearchRewrite #" nil "SearchRewrite")
      ("Show" nil "Show #." nil "Show")
@@ -626,6 +630,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 +1341,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
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 ()
diff --git a/coq/coq.el b/coq/coq.el
index 14a3338c..610f1c42 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
@@ -2742,15 +2735,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)
@@ -2758,6 +2749,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)
@@ -2781,7 +2773,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)
@@ -2798,7 +2790,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)
@@ -2818,7 +2810,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..c2cb3be5 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -924,18 +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, so @kbd{C-c .} is the key binding used to turn on
-electric terminator.  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.
 
 
 
@@ -4342,7 +4339,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).