diff options
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 = |