From 22be1892ee1b6030cfe9406bf72bb320dbe68be7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 12 Mar 2021 13:17:59 +0100
Subject: Slightly richer API allowing to shift the inductive in a block.

---
 test-suite/ltac2/ind.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'test-suite')

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
-- 
cgit v1.2.3