diff options
| -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 3fb7009564..932138f304 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1233,7 +1233,7 @@ and match_current pb tomatch = Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; let inst = List.map mkRel deps in { uj_val = applist (case, inst); - uj_type = substl inst typ } + uj_type = prod_applist typ inst } and compile_branch current names deps pb arsign eqn cstr = let sign, pb = build_branch current deps names pb arsign eqn cstr in |