From f55434e7410a4c41c31145f194950c410bec0253 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Thu, 13 Apr 2017 17:54:55 +0200
Subject: Fix compilation with camlp5 transitional mode.

It was failing after 1d0eb5d4d6fea.
---
 grammar/argextend.mlp    | 8 +++++++-
 grammar/tacextend.mlp    | 8 ++++----
 grammar/vernacextend.mlp | 8 ++++----
 3 files changed, 15 insertions(+), 9 deletions(-)

(limited to 'grammar')

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 =
-- 
cgit v1.2.3