diff options
author | 2003-09-05 12:07:21 +0000 | |
---|---|---|
committer | 2003-09-05 12:07:21 +0000 | |
commit | a677b6c61c7985768febfa4339a720b48e8f51a6 (patch) | |
tree | 5bb15afd813b3c1d39cd34a2a945cf5d0a343bbf | |
parent | 0fd335e25cdf37d734f279bc0bd562809bddb86f (diff) |
Impression sans ',' des constructeurs de meme type, pour v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4301 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | parsing/prettyp.ml | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 5ccf11bdb..41a61e5c0 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -102,20 +102,11 @@ let print_params env params = else (pr_rel_context env params ++ brk(1,2)) -let rec contract_types = function - | [] -> [] - | (id,c)::l -> - match contract_types l with - | (idl,c')::l' when eq_constr c c' -> (id::idl,c')::l' - | l' -> ([id],c)::l' - let print_constructors envpar names types = let pc = prlist_with_sep (fun () -> brk(1,0) ++ str "| ") - (fun (id,c) -> prlist_with_sep pr_coma pr_id id ++ str " : " ++ - prterm_env envpar c) - (contract_types - (Array.to_list (array_map2 (fun n t -> (n,t)) names types))) + (fun (id,c) -> pr_id id ++ str " : " ++ prterm_env envpar c) + (Array.to_list (array_map2 (fun n t -> (n,t)) names types)) in hv 0 (str " " ++ pc) |