diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-13 12:44:16 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-13 12:44:16 +0000 |
| commit | ad74962cf5b1ec9a31e56ccd9caa0c1cc98f2964 (patch) | |
| tree | f6511f1b33f629876bb2131f261ef3361a4a87da | |
| parent | 556751099326b259b5f16a693af09c7642a03d82 (diff) | |
Correction bug #1491
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9761 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 9c6582bec..93fd7704e 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 |