diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-02 06:27:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-02 06:27:05 +0000 |
| commit | 1a29faa00f1e2a6f2d71088a769fe2fbc823244a (patch) | |
| tree | 9cf1e89a8ff0473b7a87e47faf0ac53596126301 /parsing | |
| parent | a42f6a26ccf8f3d39d21ddba04885b5c476ad6cb (diff) | |
Correction oubli du cas pas d'arguments implicites du tout
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5414 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/prettyp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index aeca4a975..85442c0af 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -86,7 +86,7 @@ let need_expansion impl ref = let typ = Global.type_of_global ref in let ctx = fst (decompose_prod_assum typ) in let nprods = List.length (List.filter (fun (_,b,_) -> b=None) ctx) in - let _,lastimpl = list_chop nprods impl in + impl <> [] & let _,lastimpl = list_chop nprods impl in List.filter is_status_implicit lastimpl <> [] let print_name_infos ref = |