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 | |
| 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')
| -rw-r--r-- | parsing/g_constr.ml4 | 4 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 5 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 4 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 2 |
4 files changed, 1 insertions, 14 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index f60d06857d..abd1607d67 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -170,9 +170,7 @@ GEXTEND Gram | c1 = operconstr; ":>" -> CCast(loc,c1, CastCoerce) ] | "99" RIGHTA [ ] - | "90" RIGHTA - [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2) - | c1 = operconstr; "->"; c2 = SELF -> CArrow(loc,c1,c2)] + | "90" RIGHTA [ ] | "10" LEFTA [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args) | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) 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 ( diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 1e0f2aef2a..c4c8579d95 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -296,10 +296,6 @@ let strip_prod_binders_expr n ty = let bll = List.map (fun (x, _, y) -> x, y) bll in if nb >= n then (List.rev (bll@acc)), a else strip_ty (bll@acc) (n-nb) a - | Topconstr.CArrow(_,a,b) -> - if n=1 then - (List.rev (([(dummy_loc,Anonymous)],a)::acc), b) - else strip_ty (([(dummy_loc,Anonymous)],a)::acc) (n-1) b | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index df25972082..f364652077 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -135,8 +135,6 @@ let rec mlexpr_of_constr = function | Topconstr.CRef r -> <:expr< Topconstr.CRef $mlexpr_of_reference r$ >> | Topconstr.CFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" | Topconstr.CCoFix (loc,_,_) -> failwith "mlexpr_of_constr: TODO" - | Topconstr.CArrow (loc,a,b) -> - <:expr< Topconstr.CArrow $dloc$ $mlexpr_of_constr a$ $mlexpr_of_constr b$ >> | Topconstr.CProdN (loc,l,a) -> <:expr< Topconstr.CProdN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >> | Topconstr.CLambdaN (loc,l,a) -> <:expr< Topconstr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_binder_kind mlexpr_of_constr) l$ $mlexpr_of_constr a$ >> |