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
---
 toplevel/vernacentries.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5787feb05d..acfbaa14f5 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -952,6 +952,7 @@ let _ =
       optkey   = ["Printing";"Existential";"Instances"];
       optread  = (fun () -> !Constrextern.print_evar_arguments);
       optwrite = (:=) Constrextern.print_evar_arguments }
+
 let _ =
   declare_bool_option
     { optsync  = true;
@@ -1095,6 +1096,15 @@ let _ =
       optread  = (fun () -> get_debug () <> Tactic_debug.DebugOff);
       optwrite = vernac_debug }
 
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "explicitly parsing implicit arguments";
+      optkey   = ["Parsing";"Explicit"];
+      optread  = (fun () -> !Constrintern.parsing_explicit);
+      optwrite = (fun b ->  Constrintern.parsing_explicit := b) }
+
 let vernac_set_opacity local str =
   let glob_ref r =
     match smart_global r with
-- 
cgit v1.2.3