From be76b6af359ea61bc71e59efb4802ff01cce728c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 27 Mar 2010 15:57:02 +0000
Subject: Fixing bug #2279 (printing nested let-in was in exponential time)

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

(limited to 'pretyping')

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 905bb49e0b..6560f7b48d 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -327,7 +327,6 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
             n, aliastyp, Some typ
   in
   let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
-  let eqnl = detype_eqns constructs consnargsl bl in
   let tag =
     try
       if !Flags.raw_print then
@@ -355,8 +354,10 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
 	RIf (dl,tomatch,(alias,pred),
              Option.get nondepbrs.(0),Option.get nondepbrs.(1))
       else
+	let eqnl = detype_eqns constructs consnargsl bl in
 	RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
   | _ ->
+      let eqnl = detype_eqns constructs consnargsl bl in
       RCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
 let detype_sort = function
-- 
cgit v1.2.3