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

3 files changed, 18 insertions, 3 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)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7b0d4ff2b8..f36d56b83f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -166,6 +166,8 @@ let error_parameter_not_implicit loc =
 (* Pre-computing the implicit arguments and arguments scopes needed   *)
 (* for interpretation *)
 
+let parsing_explicit = ref false
+
 let empty_internalization_env = Idmap.empty
 
 let compute_explicitable_implicit imps = function
@@ -1215,6 +1217,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
     | CRef ref as x ->
 	let (c,imp,subscopes,l),_ =
 	  intern_applied_reference intern env (Environ.named_context globalenv) lvar [] ref in
+        assert (l=[]);
 	(match intern_impargs c env imp subscopes l with
            | [] -> c
            | l -> GApp (constr_loc x, c, l))
@@ -1333,7 +1336,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
                 find_appl_head_data c, args
             | x -> (intern env f,[],[],[]), args in
 	let args =
-	  intern_impargs c env impargs args_scopes (merge_impargs l args) in
+          intern_impargs c env impargs args_scopes (merge_impargs l args) in
 	check_projection isproj (List.length args) c;
 	(match c with
           (* Now compact "(f args') args" *)
@@ -1490,6 +1493,12 @@ let internalize sigma globalenv env allow_patvar lvar c =
   and intern_impargs c env l subscopes args =
     let l = select_impargs_size (List.length args) l in
     let eargs, rargs = extract_explicit_arg l args in
+    if !parsing_explicit then
+      if eargs <> [] then
+        error "Arguments given by name or position not supported in explicit mode."
+      else
+        intern_args env subscopes rargs
+    else
     let rec aux n impl subscopes eargs rargs =
       let (enva,subscopes') = apply_scope_env env subscopes in
       match (impl,rargs) with
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