diff options
| author | pboutill | 2012-04-12 20:49:11 +0000 |
|---|---|---|
| committer | pboutill | 2012-04-12 20:49:11 +0000 |
| commit | 3e70ea9c0967725bd320a6387d19cfb9d5a9b7fe (patch) | |
| tree | d1804bed966aefae16dff65c41a27fa0ba5a9bce /parsing/ppconstr.ml | |
| parent | 8d0136caf2458c2a2457550b1af1299098b1d038 (diff) | |
"A -> B" is a notation for "forall _ : A, B".
No good reason for that except uniformity so revert this commit if you find a
reason against it.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15146 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/ppconstr.ml')
| -rw-r--r-- | parsing/ppconstr.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 20479fe148..98ed6883e2 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -309,7 +309,6 @@ let rename na na' t c = | _ -> (na',t,c) let split_product na' = function - | CArrow (loc,t,c) -> (na',t,c) | CProdN (loc,[[na],bk,t],c) -> rename na na' t c | CProdN (loc,([na],bk,t)::bl,c) -> rename na na' t (CProdN(loc,bl,c)) | CProdN (loc,(na::nal,bk,t)::bl,c) -> @@ -428,10 +427,6 @@ let pr pr sep inherited a = pr_recursive (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix), lfix - | CArrow (_,a,b) -> - hov 0 (pr mt (larrow,L) a ++ str " ->" ++ - pr (fun () ->brk(1,0)) (-larrow,E) b), - larrow | CProdN _ -> let (bl,a) = extract_prod_binders a in hov 0 ( |