From 4204aa78b9ae084d98bc7a585ec199f94bb7ece5 Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 8 Mar 2004 17:53:03 +0000
Subject: correction de bugs des points fixes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5440 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/detyping.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index e1f0da13b5..8bd6a1a018 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -387,7 +387,7 @@ and share_names tenv n l avoid env c t =
   if !Options.v7 && n=0 then
     let c = detype tenv avoid env c in
     let t = detype tenv avoid env t in
-    (l,c,t)
+    (List.rev l,c,t)
   else
   match kind_of_term c, kind_of_term t with
     | Lambda (na,t,c), Prod (na',t',c') ->
@@ -420,7 +420,7 @@ and share_names tenv n l avoid env c t =
         if n>0 then warning "Detyping.detype: cannot factorize fix enough";
         let c = detype tenv avoid env c in
         let t = detype tenv avoid env t in
-        (l,c,t)
+        (List.rev l,c,t)
 
 and detype_eqn tenv avoid env constr construct_nargs branch =
   let make_pat x avoid env b ids =
-- 
cgit v1.2.3