Mise en place d'implicites par noms en v8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4430 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 19 insertions, 5 deletions

diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index bf26f02ec..d39be3919 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -47,7 +47,19 @@ let print_impl_args_by_pos = function
       prlist_with_sep (fun () -> str "; ") int l ++
       str"] are implicit" ++ fnl()
 
-let print_impl_args l = print_impl_args_by_pos (positions_of_implicits l)
+let print_impl_args_by_name = function
+  | []  -> mt ()
+  | [i] -> str"Argument " ++ pr_id (name_of_implicit i) ++ str" is implicit" ++
+      fnl()
+  | l   -> 
+      str"Arguments " ++ 
+      prlist_with_sep (fun () -> str ", ")
+        (fun imp -> pr_id (name_of_implicit imp)) l ++
+      str" are implicit" ++ fnl()
+
+let print_impl_args l = 
+  if !Options.v7 then print_impl_args_by_pos (positions_of_implicits l)
+  else print_impl_args_by_name (List.filter is_status_implicit l)
 
 let print_argument_scopes = function
   | [Some sc] -> str"Argument scope is [" ++ str sc ++ str"]" ++ fnl()
@@ -58,6 +70,10 @@ let print_argument_scopes = function
       str "]") ++ fnl()
   | _  -> mt()
 
+let print_name_infos ref =
+  print_impl_args (implicits_of_global ref) ++
+  print_argument_scopes (Symbols.find_arguments_scope ref)
+
 (* To be improved; the type should be used to provide the types in the
    abstractions. This should be done recursively inside prterm, so that
    the pretty-print of a proposition (P:(nat->nat)->Prop)(P [u]u)
@@ -163,8 +179,7 @@ let print_mutual sp =
 let print_section_variable sp =
   let d = get_variable sp in
   print_named_decl d ++ 
-  print_impl_args (implicits_of_global (VarRef sp)) ++
-  print_argument_scopes (Symbols.find_arguments_scope (VarRef sp))
+  print_name_infos (VarRef sp)
 
 let print_body = function
   | Some lc  -> prterm (Declarations.force lc)
@@ -187,8 +202,7 @@ let print_constant with_values sep sp =
 	print_basename sp ++ str sep ++ cut () ++
 	(if with_values then print_typed_body (val_0,typ) else prtype typ) ++
 	fnl ()) ++ 
-  print_impl_args (implicits_of_global (ConstRef sp)) ++
-  print_argument_scopes (Symbols.find_arguments_scope (ConstRef sp))
+  print_name_infos (ConstRef sp)
 
 let print_inductive sp = (print_mutual sp)