diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ltac2/ind.v | 5 |
1 files changed, 3 insertions, 2 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 |