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

6 files changed, 39 insertions, 6 deletions

diff --git a/CHANGES b/CHANGES
index 1334aa739f..cadfec6b89 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,8 +5,16 @@ Tactics
 
 - Tactics btauto, a reflexive boolean tautology solver.
 
-Changes from V8.3 to V8.4
-=========================
+Changes from V8.4beta to V8.4
+=============================
+
+Vernacular commands
+
+- New command "Set Parsing Explicit" for deactivating parsing (and printing)
+  of implicit arguments (useful for teaching).
+
+Changes from V8.3 to V8.4beta
+=============================
 
 Logic
 
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 6a42678e4f..40a5a8225a 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -105,12 +105,12 @@ Notation
 Dumpglob
 Reserve
 Impargs
-Constrextern
 Syntax_def
 Implicit_quantifiers
 Smartlocate
 Constrintern
 Modintern
+Constrextern
 Tacexpr
 Proof_type
 Goal
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
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