aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-04-13 17:54:55 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-04-14 00:27:52 +0200
commitf55434e7410a4c41c31145f194950c410bec0253 (patch)
treeffbb9b7b02ebdbc396cf174b11b622f39dc4a485
parent8b1b6e76a6229d9c091bf805e3786bdf0038ae32 (diff)
Fix compilation with camlp5 transitional mode.
It was failing after 1d0eb5d4d6fea.
-rw-r--r--grammar/argextend.mlp8
-rw-r--r--grammar/tacextend.mlp8
-rw-r--r--grammar/vernacextend.mlp8
3 files changed, 15 insertions, 9 deletions
diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
index aaf3afe43..d00ee4e5d 100644
--- a/grammar/argextend.mlp
+++ b/grammar/argextend.mlp
@@ -11,8 +11,14 @@ open Q_util
let loc = Ploc.dummy
let default_loc = <:expr< Loc.ghost >>
+IFDEF STRICT THEN
+ let ploc_vala x = Ploc.VaVal x
+ELSE
+ let ploc_vala x = x
+END
+
let declare_str_items loc l =
- MLast.StDcl (loc, Ploc.VaVal l) (* correspond to <:str_item< declare $list:l'$ end >> *)
+ MLast.StDcl (loc, ploc_vala l) (* correspond to <:str_item< declare $list:l'$ end >> *)
let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >>
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index f57be9022..1dd8da12a 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -14,11 +14,11 @@ open Argextend
(** Quotation difference for match clauses *)
let default_patt loc =
- (<:patt< _ >>, Ploc.VaVal None, <:expr< failwith "Extension: cannot occur" >>)
+ (<:patt< _ >>, ploc_vala None, <:expr< failwith "Extension: cannot occur" >>)
let make_fun loc cl =
let l = cl @ [default_patt loc] in
- MLast.ExFun (loc, Ploc.VaVal l) (* correspond to <:expr< fun [ $list:l$ ] >> *)
+ MLast.ExFun (loc, ploc_vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *)
let dloc = <:expr< Loc.ghost >>
@@ -49,7 +49,7 @@ let rec make_let raw e = function
let make_clause (pt,_,e) =
(make_patt pt,
- Ploc.VaVal None,
+ ploc_vala None,
make_let false e pt)
let make_fun_clauses loc s l =
@@ -108,7 +108,7 @@ let declare_tactic loc tacname ~level classification clause = match clause with
whole-prof tactics like [shelve_unifiable]. *)
<:expr< fun _ $lid:"ist"$ -> $tac$ >>
| _ ->
- let f = make_fun loc [patt, Ploc.VaVal None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
+ let f = make_fun loc [patt, ploc_vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in
<:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >>
in
(** Arguments are not passed directly to the ML tactic in the TacML node,
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 =