diff --git a/doc/changelog/06-Ltac2-language/17534-ltac2-0arg-empty.rst b/doc/changelog/06-Ltac2-language/17534-ltac2-0arg-empty.rst
new file mode 100644
index 000000000000..960c74761977
--- /dev/null
+++ b/doc/changelog/06-Ltac2-language/17534-ltac2-0arg-empty.rst
@@ -0,0 +1,4 @@
+- **Changed:**
+  `Array.empty`, `Message.Format.stop` and `Pattern.empty_context` are not thunked
+  (`#17534 <https://github.com/coq/coq/pull/17534>`_,
+  by Gaëtan Gilbert).
diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml
index f7792eeeeb0f..30f5bf221c6d 100644
--- a/plugins/ltac2/tac2core.ml
+++ b/plugins/ltac2/tac2core.ml
@@ -273,7 +273,7 @@ let () =
 
 let () = define "message_concat" (pp @-> pp @-> ret pp) Pp.app
 
-let () = define "format_stop" (unit @-> ret format) (fun _ -> [])
+let () = define "format_stop" (ret format) []
 
 let () =
   define "format_string" (format @-> ret format) @@ fun s ->
@@ -346,7 +346,7 @@ let () =
 
 (** Array *)
 
-let () = define "array_empty" (unit @-> ret valexpr) (fun _ -> v_blk 0 [||])
+let () = define "array_empty" (ret valexpr) (v_blk 0 [||])
 
 let () =
   define "array_make" (int @-> valexpr @-> tac valexpr) @@ fun n x ->
@@ -816,8 +816,8 @@ let () =
 
 let () =
   define "pattern_empty_context"
-    (unit @-> ret (repr_ext val_matching_context))
-    (fun _ -> Constr_matching.empty_context)
+    (ret (repr_ext val_matching_context))
+    Constr_matching.empty_context
 
 let () =
   define "pattern_matches" (pattern @-> constr @-> tac valexpr) @@ fun pat c ->
diff --git a/plugins/ltac2/tac2quote.ml b/plugins/ltac2/tac2quote.ml
index 86b710f74950..792391b87c37 100644
--- a/plugins/ltac2/tac2quote.ml
+++ b/plugins/ltac2/tac2quote.ml
@@ -553,5 +553,5 @@ let of_format { v = fmt; loc } =
     with Tac2print.InvalidFormat ->
       CErrors.user_err ?loc (str "Invalid format")
   in
-  let stop = CAst.make @@ CTacApp (global_ref (kername format_prefix "stop"), [of_tuple []]) in
+  let stop = global_ref (kername format_prefix "stop") in
   List.fold_left of_format stop fmt
diff --git a/test-suite/ltac2/array_lib.v b/test-suite/ltac2/array_lib.v
index 8ad6301b5ade..8afdb3f78176 100644
--- a/test-suite/ltac2/array_lib.v
+++ b/test-suite/ltac2/array_lib.v
@@ -45,14 +45,14 @@ Goal True.
   Fail check_eq_int ((init 3 (fun i => (Int.add i 10)))) [10;11;13].
 
   (* test empty with int *)
-  check_eq_int (empty ()) [].
-  check_eq_int (append (empty ()) (init 3 (fun i => (Int.add i 10)))) [10;11;12].
-  check_eq_int (append (init 3 (fun i => (Int.add i 10))) (empty ())) [10;11;12].
+  check_eq_int empty [].
+  check_eq_int (append empty (init 3 (fun i => (Int.add i 10)))) [10;11;12].
+  check_eq_int (append (init 3 (fun i => (Int.add i 10))) empty) [10;11;12].
 
   (* test empty with bool *)
-  check_eq_bool (empty ()) [].
-  check_eq_bool (append (empty ()) (init 3 (fun i => (Int.ge i 2)))) [false;false;true].
-  check_eq_bool (append (init 3 (fun i => (Int.ge i 2))) (empty ())) [false;false;true].
+  check_eq_bool empty [].
+  check_eq_bool (append empty (init 3 (fun i => (Int.ge i 2)))) [false;false;true].
+  check_eq_bool (append (init 3 (fun i => (Int.ge i 2))) empty) [false;false;true].
 
   (* test init with int *)
   check_eq_int (init 0 (fun i => (Int.add i 10))) [].
diff --git a/test-suite/ltac2/fragile_matching.v b/test-suite/ltac2/fragile_matching.v
index 92fed9b5809e..16423a48a684 100644
--- a/test-suite/ltac2/fragile_matching.v
+++ b/test-suite/ltac2/fragile_matching.v
@@ -109,7 +109,7 @@ Module RealCodeTest.
             } =>
             true
           end)
-        (Array.empty ())
+        Array.empty
     }.
 
 End RealCodeTest.
diff --git a/theories/Compat/Coq817.v b/theories/Compat/Coq817.v
index 8e8127c229a0..3ca9586e491a 100644
--- a/theories/Compat/Coq817.v
+++ b/theories/Compat/Coq817.v
@@ -10,12 +10,12 @@
 
 (** Compatibility file for making Coq act similar to Coq v8.17 *)
 
+Local Set Warnings "-masking-absolute-name".
+
 Require Export Coq.Compat.Coq818.
 
 Require Coq.Lists.ListSet.
 
-Local Set Warnings "-masking-absolute-name".
-
 Module Export Coq.
   Module Export Lists.
     Module Export ListSet.
diff --git a/theories/Compat/Coq818.v b/theories/Compat/Coq818.v
index 45539d10f1d9..56947964c10d 100644
--- a/theories/Compat/Coq818.v
+++ b/theories/Compat/Coq818.v
@@ -55,3 +55,14 @@ Ltac Z.euclidean_division_equations_cleanup ::=
          | [ H : ?A -> ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H
          | [ H : ?A -> ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H
          end.
+
+Local Set Warnings "-masking-absolute-name".
+
+Require Ltac2.Array.
+
+Module Export Ltac2.
+  Module Array.
+    Export Ltac2.Array.
+    Ltac2 empty () := empty.
+  End Array.
+End Ltac2.
diff --git a/user-contrib/Ltac2/Array.v b/user-contrib/Ltac2/Array.v
index f0b413fb2368..d6864ef9ef28 100644
--- a/user-contrib/Ltac2/Array.v
+++ b/user-contrib/Ltac2/Array.v
@@ -34,7 +34,7 @@ Require Ltac2.Message.
 (* Question: what is returned in case of an out of range value?
    Answer:   Ltac2 throws a panic *)
 
-Ltac2 @external empty : unit -> 'a array := "coq-core.plugins.ltac2" "array_empty".
+Ltac2 @external empty : 'a array := "coq-core.plugins.ltac2" "array_empty".
 Ltac2 @external make : int -> 'a -> 'a array := "coq-core.plugins.ltac2" "array_make".
 Ltac2 @external length : 'a array -> int := "coq-core.plugins.ltac2" "array_length".
 Ltac2 @external get : 'a array -> int -> 'a := "coq-core.plugins.ltac2" "array_get".
@@ -48,7 +48,7 @@ Ltac2 @external concat : ('a array) list -> 'a array := "coq-core.plugins.ltac2"
 Ltac2 lowlevel_sub (arr : 'a array) (start : int) (len : int) :=
   let l := length arr in
   match Int.equal l 0 with
-  | true => empty ()
+  | true => empty
   | false =>
       let newarr:=make len (get arr 0) in
       lowlevel_blit arr start newarr 0 len;
@@ -67,7 +67,7 @@ Ltac2 init (l : int) (f : int->'a) :=
     end
   in
   match Int.le l 0 with
-  | true => empty ()
+  | true => empty
   | false =>
       let arr:=make l (f 0) in
       init_aux arr 1 (Int.sub l 1) f;
@@ -174,7 +174,7 @@ Ltac2 of_list (ls : 'a list) :=
     | _ :: tl => Int.add 1 (list_length tl)
     end in
   match ls with
-  | [] => empty ()
+  | [] => empty
   | hd::tl =>
       let anew := make (list_length ls) hd in
       of_list_aux ls anew 0;
diff --git a/user-contrib/Ltac2/Message.v b/user-contrib/Ltac2/Message.v
index ffefc482509e..7c78e50b925b 100644
--- a/user-contrib/Ltac2/Message.v
+++ b/user-contrib/Ltac2/Message.v
@@ -32,7 +32,7 @@ Module Format.
 
 (** Only for internal use. *)
 
-Ltac2 @ external stop : unit -> ('a, 'b, 'c, 'a) format := "coq-core.plugins.ltac2" "format_stop".
+Ltac2 @ external stop : ('a, 'b, 'c, 'a) format := "coq-core.plugins.ltac2" "format_stop".
 
 Ltac2 @ external string : ('a, 'b, 'c, 'd) format ->
   (string -> 'a, 'b, 'c, 'd) format := "coq-core.plugins.ltac2" "format_string".
diff --git a/user-contrib/Ltac2/Pattern.v b/user-contrib/Ltac2/Pattern.v
index 0f726723b542..bf18faef28ae 100644
--- a/user-contrib/Ltac2/Pattern.v
+++ b/user-contrib/Ltac2/Pattern.v
@@ -20,7 +20,7 @@ Ltac2 Type match_kind := [
 | MatchContext
 ].
 
-Ltac2 @ external empty_context : unit -> context :=
+Ltac2 @ external empty_context : context :=
   "coq-core.plugins.ltac2" "pattern_empty_context".
 (** A trivial context only made of the hole. *)
 
@@ -88,7 +88,7 @@ Ltac2 lazy_match0 t (pats:'a constr_matching) :=
     let p := match knd with
     | MatchPattern =>
       (fun _ =>
-        let context := empty_context () in
+        let context := empty_context in
         let bind := matches_vect pat t in
         fun _ => f context bind)
     | MatchContext =>
@@ -109,7 +109,7 @@ Ltac2 multi_match0 t (pats:'a constr_matching) :=
     let p := match knd with
     | MatchPattern =>
       (fun _ =>
-        let context := empty_context () in
+        let context := empty_context in
         let bind := matches_vect pat t in
         f context bind)
     | MatchContext =>