diff --git a/ci/simple-tests/coq-test-queries.el b/ci/simple-tests/coq-test-queries.el
index 24057a10f..0e26e7485 100644
--- a/ci/simple-tests/coq-test-queries.el
+++ b/ci/simple-tests/coq-test-queries.el
@@ -37,6 +37,7 @@
 (defvar coq-ask-printing-width-function)
 (defvar coq-shell-current-line-width)
 (defvar coq-use-yasnippet)
+(defvar coq-menu-common-entries)
 
 (declare-function proof-shell-exit "proof-shell")
 (declare-function proof-shell-invisible-command "proof-shell")
@@ -52,6 +53,7 @@
 (declare-function coq-insert-as-in-next-command "coq-queries")
 (declare-function coq-run-query "coq-queries")
 (declare-function coq-About "coq-queries")
+(declare-function coq-Print-implicit "coq-queries")
 (declare-function coq-Check "coq-queries")
 (declare-function coq-Search "coq-queries")
 (declare-function coq-id-under-mouse-query "coq-queries")
@@ -316,6 +318,31 @@ query."
     (should (string-match-p "Nat\\.add" (coq-test-queries-response)))
     (should (coq-flag-is-on-p "Test Printing Notations"))))
 
+(ert-deftest coq-test-queries-menu-commands ()
+  "The menu entries of the printing flags run the flag they name."
+  (require 'coq-abbrev)
+  (let (entries)
+    (cl-labels ((walk (menu)
+                  (dolist (item menu)
+                    (cond ((vectorp item) (push item entries))
+                          ((consp item) (walk (cdr item)))))))
+      (walk coq-menu-common-entries))
+    (dolist (item entries)
+      (let ((label (aref item 0))
+            (re "\\`\\(Set\\|Unset\\) Printing \\(.*\\)\\'"))
+        (when (and (string-match re label)
+                   (not (equal (match-string 2 label) "Width")))
+          (let ((command (format "coq-%s-printing-%s"
+                                 (downcase (match-string 1 label))
+                                 (replace-regexp-in-string
+                                  " " "-" (downcase (match-string 2 label))))))
+            (should (equal (list label (aref item 1))
+                           (list label (intern command))))))))
+    (should (eq (aref (cl-find "Print Implicit..." entries
+                               :key (lambda (v) (aref v 0)) :test #'equal)
+                      1)
+                #'coq-Print-implicit))))
+
 (ert-deftest coq-test-queries-mouse ()
   "`coq-remap-mouse-1' binds the queries at mouse click when set, in the
 script, goals and response buffers, and unbinds them when unset."
diff --git a/ci/simple-tests/coq-test-without-pg.el b/ci/simple-tests/coq-test-without-pg.el
index 774757dfa..3cb2e920d 100644
--- a/ci/simple-tests/coq-test-without-pg.el
+++ b/ci/simple-tests/coq-test-without-pg.el
@@ -9,8 +9,8 @@
 ;; Test the part of Coq mode common to all backends, with the Proof
 ;; General backend disabled (obsolete `coq-use-pg' nil, so `coq-backend'
 ;; nil): it must not load the proof shell, and the abbrevs, the
-;; terminator command, the query and insertion commands and their keys
-;; must be there.
+;; terminator command, the query and insertion commands, their keys and
+;; the insertion menu must be there.
 
 ;;; Code:
 
@@ -22,6 +22,7 @@
 (require 'proof-site)
 (require 'ert)
 (require 'cl-lib)
+(require 'seq)
 
 (defvar coq-mode-abbrev-table)
 (defvar coq-load-path)
@@ -29,6 +30,7 @@
 (defvar coq-query-function)
 (defvar coq-use-yasnippet)
 (defvar coq-goals-count-function)
+(defvar coq-insert-menu)
 
 (declare-function coq-run-query "coq-queries")
 (declare-function coq-templates-setup "coq-templates")
@@ -174,6 +176,22 @@ indent."
     (setq-local coq-goals-count-function (lambda () '(5 . 3)))
     (should (equal (coq-goals-count) '(5 . 3)))))
 
+(ert-deftest coq-test-without-pg-insert-menu ()
+  "The menu of the insertions is defined without backend."
+  (coq-test-without-pg-with-file
+    (should (equal (car coq-insert-menu) "INSERT"))
+    (let ((commands (delq nil (mapcar (lambda (item)
+                                        (and (vectorp item) (aref item 1)))
+                                      coq-insert-menu)))
+          (submenus (mapcar #'car (seq-filter #'consp (cdr coq-insert-menu)))))
+      (dolist (command '(coq-insert-intros coq-insert-tactic
+                         coq-insert-tactical coq-insert-command
+                         coq-insert-term coq-insert-section-or-module
+                         coq-insert-requires))
+        (should (memq command commands)))
+      (should (equal submenus '("Tactics (menu)" "Tacticals (menu)"
+                                "Command (menu)" "Term (menu)"))))))
+
 (provide 'coq-test-without-pg)
 
 ;;; coq-test-without-pg.el ends here
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 65dfe493f..368e2aa2c 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -29,28 +29,6 @@
   (describe-variable 'coq-local-vars-doc))
 
 
-(defconst coq-tactics-menu
-  (append '("Tactics (menu)"
-	    ["Intros (smart)" coq-insert-intros :help "Insert \"intros h1 .. hn.\" where hi are the default names given by Coq."])
-	  (coq-build-menu-from-db (append coq-tactics-db coq-solve-tactics-db))))
-
-(defconst coq-tacticals-menu
-  (append '("Tacticals (menu)")
-	  (coq-build-menu-from-db coq-tacticals-db)))
-
-(defconst coq-commands-menu
-  (append '("Command (menu)"
-	    ;["Module/Section (smart)" coq-insert-section-or-module t]
-	    ;["Require (smart)" coq-insert-requires t]
-	    )
-	  (coq-build-menu-from-db coq-commands-db)))
-
-(defconst coq-terms-menu
-  (append '("Term (menu)"
-	    ["Match (smart)" coq-insert-match t])
-	  (coq-build-menu-from-db coq-terms-db)))
-
-
         ;; (if (fboundp 'with-undo-amalgamate) ;; emacs > 29.1
         ;;     (with-undo-amalgamate (insert abbr) (yas-expand))
         ;;   (progn (insert abbr) (yas-expand)))
@@ -317,7 +295,7 @@
      ["Print Section..." coq-PrintSection t]
      ""
      ["Locate notation..." coq-LocateNotation t]
-     ["Print Implicit..." coq-Print t]
+     ["Print Implicit..." coq-Print-implicit t]
      ["Print Scope/Visibility..." coq-PrintScope t])
     ("OPTIONS"
      ["Set Printing All" coq-set-printing-all t]
@@ -330,8 +308,8 @@
      ["Unset Printing Notations" coq-unset-printing-notations t]
      ["Set Printing Coercions" coq-set-printing-coercions t]
      ["Unset Printing Coercions" coq-unset-printing-coercions t]
-     ["Set Printing Compact Contexts" coq-set-printing-implicit t]
-     ["Unset Printing Compact Contexts" coq-unset-printing-implicit t]
+     ["Set Printing Compact Contexts" coq-set-printing-compact-contexts t]
+     ["Unset Printing Compact Contexts" coq-unset-printing-compact-contexts t]
      ["Set Printing Synth" coq-set-printing-synth t]
      ["Unset Printing Synth" coq-unset-printing-synth t]
      ["Set Printing Universes" coq-set-printing-universes t]
@@ -346,21 +324,7 @@
   (append coq-menu-common-entries
   `(
     ""
-    ("INSERT"
-     ["Intros (smart)" coq-insert-intros :help "Insert \"intros h1 .. hn.\" where hi are the default names given by Coq."]
-     ""
-     ["Tactic (interactive)" coq-insert-tactic t]
-     ["Tactical (interactive)" coq-insert-tactical t]
-     ["Command (interactive)" coq-insert-command t]
-     ["Term (interactive)" coq-insert-term t]
-     ""
-     ,coq-tactics-menu
-     ,coq-tacticals-menu
-     ,coq-commands-menu
-     ,coq-terms-menu
-     ""
-     ["Module/Section (smart)" coq-insert-section-or-module t]
-     ["Require (smart)" coq-insert-requires t])
+    ,coq-insert-menu
     ""
     ("ABBREVS"
      ["Expand At Point" expand-abbrev t]
diff --git a/coq/coq-templates.el b/coq/coq-templates.el
index 0df6ff391..fa7298688 100644
--- a/coq/coq-templates.el
+++ b/coq/coq-templates.el
@@ -92,7 +92,7 @@ Otherwise the abbrevs of `coq-mode-abbrev-table' are available."
 ;; They insert text from the keyword databases of coq-syntax.el, or
 ;; after asking questions, without any backend.
 
-(defvar coq-load-path)                  ; in coq-system.el
+(defvar coq-load-path)                  ; in coq-project.el
 
 (define-obsolete-variable-alias 'module-kinds-table
   'coq-module-kinds-table "4.6")
@@ -219,6 +219,48 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
   (interactive)
   (coq-insert-from-db coq-terms-db "Kind of term"))
 
+;; The menu of the insertions, common to all backends.  The insertions
+;; built from a query (Intros, Match) are in coq-queries.el.
+
+(defconst coq-tactics-menu
+  (append '("Tactics (menu)"
+	    ["Intros (smart)" coq-insert-intros :help "Insert \"intros h1 .. hn.\" where hi are the default names given by Coq."])
+	  (coq-build-menu-from-db (append coq-tactics-db coq-solve-tactics-db))))
+
+(defconst coq-tacticals-menu
+  (append '("Tacticals (menu)")
+	  (coq-build-menu-from-db coq-tacticals-db)))
+
+(defconst coq-commands-menu
+  (append '("Command (menu)"
+	    ;["Module/Section (smart)" coq-insert-section-or-module t]
+	    ;["Require (smart)" coq-insert-requires t]
+	    )
+	  (coq-build-menu-from-db coq-commands-db)))
+
+(defconst coq-terms-menu
+  (append '("Term (menu)"
+	    ["Match (smart)" coq-insert-match t])
+	  (coq-build-menu-from-db coq-terms-db)))
+
+(defconst coq-insert-menu
+  `("INSERT"
+    ["Intros (smart)" coq-insert-intros :help "Insert \"intros h1 .. hn.\" where hi are the default names given by Coq."]
+    ""
+    ["Tactic (interactive)" coq-insert-tactic t]
+    ["Tactical (interactive)" coq-insert-tactical t]
+    ["Command (interactive)" coq-insert-command t]
+    ["Term (interactive)" coq-insert-term t]
+    ""
+    ,coq-tactics-menu
+    ,coq-tacticals-menu
+    ,coq-commands-menu
+    ,coq-terms-menu
+    ""
+    ["Module/Section (smart)" coq-insert-section-or-module t]
+    ["Require (smart)" coq-insert-requires t])
+  "Menu of the insertions, common to all Coq backends.")
+
 (provide 'coq-templates)
 
 ;;; coq-templates.el ends here