From e9459e5f6fb46a0ad99a474c98a496417aee17a0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 28 Sep 2023 17:08:32 +0200 Subject: [PATCH] Ltac2: remove redundant constr_constructor external --- plugins/ltac2/tac2core.ml | 11 ----------- user-contrib/Ltac2/Constr.v | 4 +++- 2 files changed, 3 insertions(+), 12 deletions(-) diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index 02d9c0cfd8d4..e310ec0421d9 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -684,17 +684,6 @@ let () = define "constr_cast_default" (ret valexpr) (of_cast DEFAULTcast) let () = define "constr_cast_vm" (ret valexpr) (of_cast VMcast) let () = define "constr_cast_native" (ret valexpr) (of_cast NATIVEcast) -let () = - define "constr_constructor" (repr_ext val_inductive @-> int @-> tac valexpr) @@ fun (ind, i) k -> - Proofview.tclENV >>= fun env -> - try - let open Declarations in - let ans = Environ.lookup_mind ind env in - let _ = ans.mind_packets.(i).mind_consnames.(k) in - return (Value.of_ext val_constructor ((ind, i), (k + 1))) - with e when CErrors.noncritical e -> - throw err_notfound - let () = define "constr_in_context" (ident @-> constr @-> closure @-> tac constr) @@ fun id t c -> Proofview.Goal.goals >>= function diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v index df6a4af8ef1a..4bbd6efab5da 100644 --- a/user-contrib/Ltac2/Constr.v +++ b/user-contrib/Ltac2/Constr.v @@ -9,6 +9,7 @@ (************************************************************************) Require Import Ltac2.Init. +Require Ltac2.Ind. Ltac2 @ external type : constr -> constr := "coq-core.plugins.ltac2" "constr_type". (** Return the type of a term *) @@ -88,7 +89,8 @@ Ltac2 occurn (n : int) (c : constr) : bool := occur_between n 1 c. Ltac2 @ external case : inductive -> case := "coq-core.plugins.ltac2" "constr_case". (** Generate the case information for a given inductive type. *) -Ltac2 @ external constructor : inductive -> int -> constructor := "coq-core.plugins.ltac2" "constr_constructor". +Ltac2 constructor (ind : inductive) (i : int) : constructor := + Ind.get_constructor (Ind.data ind) i. (** Generate the i-th constructor for a given inductive type. Indexing starts at 0. Panics if there is no such constructor. *)