Use Ltac2.Array.make 0 instead of Array.empty for compat (coq/coq…

…#17534)
SkySkimmer · Nov 22, 2023 · 676f556 · 676f556
1 parent 4b3074b
commit 676f556
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/src/coqutil/Tactics/RecordEta.v b/src/coqutil/Tactics/RecordEta.v
@@ -33,7 +33,10 @@ Ltac2 constructor_of_record(t: constr) :=
 Ltac2 eta(t: constr) :=
   let (h, args) := match Constr.Unsafe.kind t with
                    | Constr.Unsafe.App h args => (h, args)
-                   | _ => (t, Array.empty ())
+                   | _ =>
+                       (* Array.make 0 instead of Array.empty for compat
+                          (<8.19 Array.empty takes unit argument) *)
+                       (t, Array.make 0 'Prop)
                    end in
   let ctor := constructor_of_record h in
   let getters := List.map (fun getterRef => mkApp (Env.instantiate getterRef) args)

diff --git a/src/coqutil/Tactics/Records.v b/src/coqutil/Tactics/Records.v
@@ -14,7 +14,10 @@ Ltac2 head(c: constr) :=
 Ltac2 splitApp(c: constr) :=
   match Constr.Unsafe.kind c with
   | Constr.Unsafe.App f args => (f, args)
-  | _ => (c, Array.empty ())
+  | _ =>
+      (* Array.make 0 instead of Array.empty for compat
+         (<8.19 Array.empty takes unit argument) *)
+      (c, Array.make 0 'Prop)
   end.
 
 Ltac2 mkApp(c: constr)(args: constr array) :=