diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-30 14:35:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-30 14:35:58 +0000 |
| commit | e136645178f91b821bb444fa86f615caa1873c1c (patch) | |
| tree | bcf4991891bfdd95e34ed50c48aa6330826ae4c7 /parsing | |
| parent | 984890d972aaa0586b509058dc4fcea5f2c3ca2d (diff) | |
Quick improvement of some error messages related to module application
(localization of the error and hopefully improved messages)
[Is there a reason why the restriction is not enforced at the parsing level?
Anyway, treating it at interpretation time allows more appropriate messages]
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14422 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 7 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 6 |
2 files changed, 7 insertions, 6 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 965091683..e27fcca27 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -485,7 +485,7 @@ GEXTEND Gram (* Module expressions *) module_expr: [ [ me = module_expr_atom -> me - | me1 = module_expr; me2 = module_expr_atom -> CMapply (me1,me2) + | me1 = module_expr; me2 = module_expr_atom -> CMapply (loc,me1,me2) ] ] ; module_expr_atom: @@ -501,8 +501,9 @@ GEXTEND Gram module_type: [ [ qid = qualid -> CMident qid | "("; mt = module_type; ")" -> mt - | mty = module_type; me = module_expr_atom -> CMapply (mty,me) - | mty = module_type; "with"; decl = with_declaration -> CMwith (mty,decl) + | mty = module_type; me = module_expr_atom -> CMapply (loc,mty,me) + | mty = module_type; "with"; decl = with_declaration -> + CMwith (loc,mty,decl) ] ] ; END diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index db6f0e621..375e071f8 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -218,13 +218,13 @@ let pr_with_declaration pr_c = function let rec pr_module_ast pr_c = function | CMident qid -> spc () ++ pr_located pr_qualid qid - | CMwith (mty,decl) -> + | CMwith (_,mty,decl) -> let m = pr_module_ast pr_c mty in let p = pr_with_declaration pr_c decl in m ++ spc() ++ str"with" ++ spc() ++ p - | CMapply (me1,(CMident _ as me2)) -> + | CMapply (_,me1,(CMident _ as me2)) -> pr_module_ast pr_c me1 ++ spc() ++ pr_module_ast pr_c me2 - | CMapply (me1,me2) -> + | CMapply (_,me1,me2) -> pr_module_ast pr_c me1 ++ spc() ++ hov 1 (str"(" ++ pr_module_ast pr_c me2 ++ str")") |