aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/ppvernac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/ppvernac.ml')
-rw-r--r--parsing/ppvernac.ml6
1 files changed, 3 insertions, 3 deletions
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")")