From 9753602f5486d82119a0ec66fb32f9be312948ac Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 29 Sep 2003 10:06:05 +0000
Subject: Oubli du type du terme a filtrer quand pas d'argument dans la
 traduction de case

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

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a0fbb77241..6abc1860c8 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -785,8 +785,11 @@ let rec pretype tycon env isevars lvar = function
                   let na,rtntyopt,_ = 
                     if dep then decomp_lam_force 1 avoid [] p
                     else [Anonymous],p,[] in
-                  let args = List.map (fun _ -> Anonymous) params @ nal in
-                  (Some rtntyopt,(List.hd na,Some (dummy_loc,ind,args))) in
+		  let intyp =
+		    if nal=[] then None else
+                      let args = List.map (fun _ -> Anonymous) params @ nal in
+		      Some (dummy_loc,ind,args) in
+                  (Some rtntyopt,(List.hd na,intyp)) in
 	    if st = IfStyle & snd indnalopt = None then
 	      (* Translate into a "if ... then ... else" *)
 	      (* TODO: translate into a "if" even if po is dependent *)
-- 
cgit v1.2.3