diff options
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 5ab9f9a02b..0c339e8b8e 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -134,7 +134,7 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = let rec names_prod_letin t = match kind_of_term t with | Prod(n,_,t) -> n::(names_prod_letin t) | LetIn(n,_,_,t) -> n::(names_prod_letin t) - | Cast(t,_) -> names_prod_letin t + | Cast(t,_,_) -> names_prod_letin t | _ -> [] in assert (Array.length mib1.mind_packets = 1); |