From ad74962cf5b1ec9a31e56ccd9caa0c1cc98f2964 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 13 Apr 2007 12:44:16 +0000
Subject: Correction bug #1491

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9761 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/tacred.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 
-- 
cgit v1.2.3