diff options
| author | herbelin | 2012-01-20 21:08:39 +0000 |
|---|---|---|
| committer | herbelin | 2012-01-20 21:08:39 +0000 |
| commit | 6679d01256ce9a4a05c13eabbb4e2d85c3e6f075 (patch) | |
| tree | f7002c72a29516eb41a5e13f807754b999879039 /interp/constrextern.ml | |
| parent | 22a8453f551349bbafa14b914aa784693dcf3615 (diff) | |
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
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 7 |
1 files changed, 5 insertions, 2 deletions
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) |