diff options
| author | herbelin | 2003-09-29 10:06:05 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-29 10:06:05 +0000 |
| commit | 9753602f5486d82119a0ec66fb32f9be312948ac (patch) | |
| tree | d3df1d7e9bbc8f089ad1a4925d60482cc4268916 | |
| parent | 5abf5d88205b9053285e2b06c79921239827caea (diff) | |
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
| -rw-r--r-- | pretyping/pretyping.ml | 7 |
1 files 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 *) |