diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-04-13 17:54:55 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-14 00:27:52 +0200 |
| commit | f55434e7410a4c41c31145f194950c410bec0253 (patch) | |
| tree | ffbb9b7b02ebdbc396cf174b11b622f39dc4a485 /grammar/vernacextend.mlp | |
| parent | 8b1b6e76a6229d9c091bf805e3786bdf0038ae32 (diff) | |
Fix compilation with camlp5 transitional mode.
It was failing after 1d0eb5d4d6fea.
Diffstat (limited to 'grammar/vernacextend.mlp')
| -rw-r--r-- | grammar/vernacextend.mlp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index d4857b1df..436a7f0d9 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -36,7 +36,7 @@ let rec make_let e = function let make_clause { r_patt = pt; r_branch = e; } = (make_patt pt, - Ploc.VaVal None, + ploc_vala None, make_let e pt) (* To avoid warnings *) @@ -54,11 +54,11 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = match c ,cg with | Some c, _ -> (make_patt pt, - Ploc.VaVal None, + ploc_vala None, make_let (mk_ignore c pt) pt) | None, Some cg -> (make_patt pt, - Ploc.VaVal None, + ploc_vala None, <:expr< fun () -> $cg$ $str:s$ >>) | None, None -> prerr_endline (("Vernac entry \""^s^"\" misses a classifier. "^ @@ -81,7 +81,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = ("Specific classifiers have precedence over global "^ "classifiers. Only one classifier is called.") ^ "\n"); (make_patt pt, - Ploc.VaVal None, + ploc_vala None, <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) let make_fun_clauses loc s l = |