From 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Tue, 19 Apr 2011 16:44:20 +0200
Subject: Imported Upstream version 8.3.pl2

---
 parsing/tacextend.ml4 | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'parsing/tacextend.ml4')

diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index f067fcf3..39477b0b 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id: tacextend.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: tacextend.ml4 13799 2011-01-25 17:38:40Z glondu $ *)
 
 open Util
 open Genarg
@@ -55,7 +55,7 @@ let rec make_let e = function
 let add_clause s (pt,e) l =
   let p = make_patt pt in
   let w = Some (make_when (MLast.loc_of_expr e) pt) in
-  (p, w, make_let e pt)::l
+  (p, <:vala< w >>, make_let e pt)::l
 
 let rec extract_signature = function
   | [] -> []
@@ -72,7 +72,8 @@ let check_unicity s l =
 let make_clauses s l =
   check_unicity s l;
   let default =
-    (<:patt< _ >>,None,<:expr< failwith "Tactic extension: cannot occur" >>) in
+    (<:patt< _ >>,<:vala<None>>,
+     <:expr< failwith "Tactic extension: cannot occur" >>) in
   List.fold_right (add_clause s) l [default]
 
 let rec make_args = function
-- 
cgit v1.2.3