diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index d80fd80758..79b048979d 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1436,7 +1436,7 @@ let rename_env subst env = let is_dependent_indtype = function | NotInd _ -> false - | IsInd (_, IndType(_,realargs)) -> List.length realargs <> 0 + | IsInd (_, IndType(_,realargs)) -> realargs <> [] let prepare_initial_alias_eqn isdep tomatchl eqn = let (subst, pats) = |