From 04e9be59051ca60bf61d5142ac14386920876926 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 18 Sep 2015 08:00:14 +0200
Subject: Do not compress match constructs when the inner match contains no
 branch. (Fix bug #4348)

---
 pretyping/detyping.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 28fb8cbe36..8bd57290b0 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -276,6 +276,7 @@ and align_tree nal isgoal (e,c as rhs) = match nal with
     match kind_of_term c with
     | Case (ci,p,c,cl) when
         eq_constr c (mkRel (List.index Name.equal na (fst (snd e))))
+        && not (Int.equal (Array.length cl) 0)
 	&& (* don't contract if p dependent *)
 	computable p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) ->
 	let clauses = build_tree na isgoal e ci cl in
-- 
cgit v1.2.3