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/constrextern.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'interp/constrextern.ml')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index dc328ce75a..be60c9c307 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -479,6 +479,7 @@ let is_needed_for_correct_partial_application tail imp =
 (* Implicit args indexes are in ascending order *)
 (* inctx is useful only if there is a last argument to be deduced from ctxt *)
 let explicitize loc inctx impl (cf,f) args =
+  let impl = if !Constrintern.parsing_explicit then [] else impl in
   let n = List.length args in
   let rec exprec q = function
     | a::args, imp::impl when is_status_implicit imp ->
@@ -514,7 +515,9 @@ let explicitize loc inctx impl (cf,f) args =
 	if args = [] then f else CApp (loc, (None, f), args)
 
 let extern_global loc impl f =
-  if impl <> [] & List.for_all is_status_implicit impl then
+  if not !Constrintern.parsing_explicit &&
+     impl <> [] && List.for_all is_status_implicit impl
+  then
     CAppExpl (loc, (None, f), [])
   else
     CRef f
@@ -523,7 +526,7 @@ let extern_app loc inctx impl (cf,f) args =
   if args = [] (* maybe caused by a hidden coercion *) then
     extern_global loc impl f
   else
-  if
+  if not !Constrintern.parsing_explicit &&
     ((!Flags.raw_print or
       (!print_implicits & not !print_implicits_explicit_args)) &
      List.exists is_status_implicit impl)
-- 
cgit v1.2.3