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
---
 parsing/q_coqast.ml4     | 2 +-
 parsing/tacextend.ml4    | 2 +-
 parsing/vernacextend.ml4 | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'parsing')

diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index d5ffa6457f..eceb02d53e 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -506,7 +506,7 @@ let rec patt_of_expr e =
   match e with
     | ExAcc (_, e1, e2) -> PaAcc (loc, patt_of_expr e1, patt_of_expr e2)
     | ExApp (_, e1, e2) -> PaApp (loc, patt_of_expr e1, patt_of_expr e2)
-    | ExLid (_, "loc") -> PaAny loc
+    | ExLid (_, x) when x = vala "loc" -> PaAny loc
     | ExLid (_, s) -> PaLid (loc, s)
     | ExUid (_, s) -> PaUid (loc, s)
     | ExStr (_, s) -> PaStr (loc, s)
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index e1ae919663..ec305ee2eb 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -59,7 +59,7 @@ let check_unicity s l =
 
 let make_clause (pt,e) =
   (make_patt pt,
-   Some (make_when (MLast.loc_of_expr e) pt),
+   vala (Some (make_when (MLast.loc_of_expr e) pt)),
    make_let e pt)
 
 let make_fun_clauses loc s l =
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 58946eda9a..cc3bd07e8a 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -36,7 +36,7 @@ let check_unicity s l =
 
 let make_clause (_,pt,e) =
   (make_patt pt,
-   Some (make_when (MLast.loc_of_expr e) pt),
+   vala (Some (make_when (MLast.loc_of_expr e) pt)),
    make_let e pt)
 
 let make_fun_clauses loc s l =
-- 
cgit v1.2.3