diff options
| author | Emilio Jesus Gallego Arias | 2017-04-09 03:35:20 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-25 00:33:36 +0200 |
| commit | ee2197096fe75a63b4d92cb3a1bb05122c5c625b (patch) | |
| tree | 3b40c06375a463625a2675b90e009fcb0b64a7d2 /printing | |
| parent | 054d2736c1c1b55cb7708ff0444af521cd0fe2ba (diff) | |
[location] [ast] Port module AST to CAst
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 8928d83b09..fded0a60bd 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -201,19 +201,19 @@ open Decl_kinds keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ pr_located pr_qualid qid - let rec pr_module_ast leading_space pr_c = function - | loc, CMident qid -> + let rec pr_module_ast leading_space pr_c = let open CAst in function + | { loc ; v = CMident qid } -> if leading_space then spc () ++ pr_located pr_qualid (loc, qid) else pr_located pr_qualid (loc,qid) - | _loc, CMwith (mty,decl) -> + | { v = CMwith (mty,decl) } -> let m = pr_module_ast leading_space pr_c mty in let p = pr_with_declaration pr_c decl in m ++ spc() ++ keyword "with" ++ spc() ++ p - | _loc, CMapply (me1,(_, CMident _ as me2)) -> + | { v = CMapply (me1, ( { v = CMident _ } as me2 ) ) } -> pr_module_ast leading_space pr_c me1 ++ spc() ++ pr_module_ast false pr_c me2 - | _loc, CMapply (me1,me2) -> + | { v = CMapply (me1,me2) } -> pr_module_ast leading_space pr_c me1 ++ spc() ++ hov 1 (str"(" ++ pr_module_ast false pr_c me2 ++ str")") |