From 6679d01256ce9a4a05c13eabbb4e2d85c3e6f075 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 20 Jan 2012 21:08:39 +0000
Subject: Added new command "Set Parsing Explicit" for deactivating parsing
 (and printing) of implicit arguments (a priori useful for teaching).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14928 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 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 be78837ff3..7d0009021d 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