From 676f556187d82e08fe989452f10440f7cd42dba0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 22 Nov 2023 16:42:14 +0100 Subject: [PATCH] Use `Ltac2.Array.make 0` instead of `Array.empty` for compat (coq/coq#17534) --- src/coqutil/Tactics/RecordEta.v | 5 ++++- src/coqutil/Tactics/Records.v | 5 ++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/coqutil/Tactics/RecordEta.v b/src/coqutil/Tactics/RecordEta.v index 3cbfb9d9..d6adddd5 100644 --- 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 index 4db0e130..718c3cc0 100644 --- 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) :=