diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/tacred.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 9c6582bec9..93fd7704e2 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -361,7 +361,7 @@ let contract_cofix_use_function f (bodynum,(names,_,bodies as typedbodies)) = | None -> mkCoFix(j,typedbodies) | Some c -> c in let subbodies = list_tabulate make_Fi nbodies in - substl subbodies bodies.(bodynum) + substl (List.rev subbodies) bodies.(bodynum) let reduce_mind_case_use_function func env mia = match kind_of_term mia.mconstr with |