From 72b9a7df489ea47b3e5470741fd39f6100d31676 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Sat, 18 Aug 2007 20:34:57 +0000
Subject: Imported Upstream version 8.1.pl1+dfsg

---
 parsing/q_constr.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'parsing/q_constr.ml4')

diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index 768bc45c..21c851df 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -73,7 +73,7 @@ EXTEND
     | "0"
       [ s = sort -> <:expr< Rawterm.RSort ($dloc$,s) >>
       | id = ident -> <:expr< Rawterm.RVar ($dloc$,$id$) >>
-      | "_" -> <:expr< Rawterm.RHole ($dloc$,QuestionMark) >>
+      | "_" -> <:expr< Rawterm.RHole ($dloc$, QuestionMark False) >>
       | "?"; id = ident -> <:expr< Rawterm.RPatVar($dloc$,(False,$id$)) >>
       | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" ->
           apply_ref <:expr< coq_sumbool_ref >> [c1;c2]
-- 
cgit v1.2.3