From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 4 Jun 2012 12:07:52 +0200
Subject: Imported Upstream version 8.4~gamma0+really8.4beta2

---
 interp/constrintern.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'interp/constrintern.mli')

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index be78837f..7d000902 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -178,5 +178,8 @@ val interp_aconstr : ?impls:internalization_env ->
   (identifier * identifier) list -> constr_expr ->
   (identifier * (subscopes * notation_var_internalization_type)) list * aconstr
 
+(** Globalization options *)
+val parsing_explicit : bool ref
+
 (** Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
-- 
cgit v1.2.3