From bc2cebecc14bee4a1a486ff0bead87b6fd69d452 Mon Sep 17 00:00:00 2001
From: glondu
Date: Tue, 25 Jan 2011 20:53:24 +0000
Subject: Fix compilation with camlp5 (Closes: #2487)

With hints from Daniel de Rauglaudre.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13802 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/compat.ml4 | 16 +++++++++++++---
 1 file changed, 13 insertions(+), 3 deletions(-)

(limited to 'lib')

diff --git a/lib/compat.ml4 b/lib/compat.ml4
index d3f28b0570..8d8483b49f 100644
--- a/lib/compat.ml4
+++ b/lib/compat.ml4
@@ -185,12 +185,22 @@ let maybe_curry f = f
 let maybe_uncurry f = f
 END
 
+(** Compatibility with camlp5 strict mode *)
+IFDEF CAMLP5 THEN
+  IFDEF STRICT THEN
+    let vala x = Ploc.VaVal x
+  ELSE
+    let vala x = x
+  END
+ELSE
+  let vala x = x
+END
 
 (** Fix a quotation difference in [str_item] *)
 
 let declare_str_items loc l =
 IFDEF CAMLP5 THEN
-  MLast.StDcl (loc,l) (* correspond to <:str_item< declare $list:l'$ end >> *)
+  MLast.StDcl (loc, vala l) (* correspond to <:str_item< declare $list:l'$ end >> *)
 ELSE
   Ast.stSem_of_list l
 END
@@ -198,13 +208,13 @@ END
 (** Quotation difference for match clauses *)
 
 let default_patt loc =
-  (<:patt< _ >>, None, <:expr< failwith "Extension: cannot occur" >>)
+  (<:patt< _ >>, vala None, <:expr< failwith "Extension: cannot occur" >>)
 
 IFDEF CAMLP5 THEN
 
 let make_fun loc cl =
   let l = cl @ [default_patt loc] in
-  MLast.ExFun (loc,l)  (* correspond to <:expr< fun [ $list:l$ ] >> *)
+  MLast.ExFun (loc, vala l)  (* correspond to <:expr< fun [ $list:l$ ] >> *)
 
 ELSE
 
-- 
cgit v1.2.3