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 42569c9ce..39191f395 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -498,7 +498,7 @@ let check_and_adjust_constructor loc (_,j as cstr_sp) mind cstrs pats = let nb_args_constr = cstrs.(j-1).cs_nargs in if List.length pats = nb_args_constr then pats else - try adjust_local_defs (pats, cstrs.(j-1).cs_args) + try adjust_local_defs (pats, List.rev cstrs.(j-1).cs_args) with NotAdjustable -> error_wrong_numarg_constructor_loc loc cstr_sp nb_args_constr |