Ltac2: remove redundant constr_constructor external

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

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. *)