3 files changed, 26 insertions, 9 deletions
diff --git a/test-suite/ltac2/ind.v b/test-suite/ltac2/ind.v
index c06ffebabe..6f7352d224 100644
--- a/test-suite/ltac2/ind.v
+++ b/test-suite/ltac2/ind.v
@@ -9,11 +9,12 @@ Ltac2 Eval
   end in
   let data := Ind.data nat in
   (* Check that there is only one inductive in the block *)
-  let ntypes := Ind.ntypes data in
+  let ntypes := Ind.nblocks data in
   let () := if Int.equal ntypes 1 then () else Control.throw Not_found in
-  let nat' := Ind.get_type data 0 in
+  let nat' := Ind.repr (Ind.get_block data 0) in
   (* Check it corresponds *)
   let () := if Ind.equal nat nat' then () else Control.throw Not_found in
+  let () := if Int.equal (Ind.index nat) 0 then () else Control.throw Not_found in
   (* Check the number of constructors *)
   let nconstr := Ind.nconstructors data in
   let () := if Int.equal nconstr 2 then () else Control.throw Not_found in
diff --git a/user-contrib/Ltac2/Ind.v b/user-contrib/Ltac2/Ind.v
index 0283cb7121..f397a0e2c8 100644
--- a/user-contrib/Ltac2/Ind.v
+++ b/user-contrib/Ltac2/Ind.v
@@ -22,15 +22,23 @@ Ltac2 @ external data : t -> data := "ltac2" "ind_data".
 (** Get the mutual blocks corresponding to an inductive type in the current
     environment. Panics if there is no such inductive. *)
 
-Ltac2 @ external ntypes : data -> int := "ltac2" "ind_ntypes".
+Ltac2 @ external repr : data -> t := "ltac2" "ind_repr".
+(** Returns the inductive corresponding to the block. Inverse of [data]. *)
+
+Ltac2 @ external index : t -> int := "ltac2" "ind_index".
+(** Returns the index of the inductive type inside its mutual block. Guaranteed
+    to range between [0] and [nblocks data - 1] where [data] was retrieved
+    using the above function. *)
+
+Ltac2 @ external nblocks : data -> int := "ltac2" "ind_nblocks".
 (** Returns the number of inductive types appearing in a mutual block. *)
 
 Ltac2 @ external nconstructors : data -> int := "ltac2" "ind_nconstructors".
 (** Returns the number of constructors appearing in the current block. *)
 
-Ltac2 @ external get_type : data -> int -> t := "ltac2" "ind_get_type".
-(** Returns the nth inductive type in the block. Index must range between [0]
-    and [ntypes data - 1], otherwise the function panics. *)
+Ltac2 @ external get_block : data -> int -> data := "ltac2" "ind_get_block".
+(** Returns the block corresponding to the nth inductive type. Index must range
+    between [0] and [nblocks data - 1], otherwise the function panics. *)
 
 Ltac2 @ external get_constructor : data -> int -> constructor := "ltac2" "ind_get_constructor".
 (** Returns the nth constructor of the inductive type. Index must range between
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index b9eef5c44e..d8fe03b7c0 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1090,7 +1090,15 @@ let () = define1 "ind_data" (repr_ext val_inductive) begin fun ind ->
     throw err_notfound
 end
 
-let () = define1 "ind_ntypes" (repr_ext val_ind_data) begin fun (ind, mib) ->
+let () = define1 "ind_repr" (repr_ext val_ind_data) begin fun (ind, _) ->
+  return (Value.of_ext val_inductive ind)
+end
+
+let () = define1 "ind_index" (repr_ext val_inductive) begin fun (ind, n) ->
+  return (Value.of_int n)
+end
+
+let () = define1 "ind_nblocks" (repr_ext val_ind_data) begin fun (ind, mib) ->
   return (Value.of_int (Array.length mib.Declarations.mind_packets))
 end
 
@@ -1099,9 +1107,9 @@ let () = define1 "ind_nconstructors" (repr_ext val_ind_data) begin fun ((_, n),
   return (Value.of_int (Array.length mib.mind_packets.(n).mind_consnames))
 end
 
-let () = define2 "ind_get_type" (repr_ext val_ind_data) int begin fun (ind, mib) n ->
+let () = define2 "ind_get_block" (repr_ext val_ind_data) int begin fun (ind, mib) n ->
   if 0 <= n && n < Array.length mib.Declarations.mind_packets then
-    return (Value.of_ext val_inductive (fst ind, n))
+    return (Value.of_ext val_ind_data ((fst ind, n), mib))
   else throw err_notfound
 end