Nouveaux changements autour des implicites (notamment suite à

discussion avec Georges)

- La notion d'insertion maximale n'est plus globale mais attachée à
  chaque implicite
- Correction de petits bugs dans le calcul des implicites
- Raffinement de la notion "sous contexte" pour l'affichage des coercions



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

3 files changed, 27 insertions, 26 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f816001578..8c6e1a547f 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -466,13 +466,17 @@ GEXTEND Gram
 	     [ local = [ IDENT "Global" -> false | IDENT "Local" -> true ];
 	       qid = global -> (local,qid,None) 
 	     | qid = global;
-	       l = OPT [ "["; l = LIST0 ident; "]" -> 
-		   List.map (fun id -> ExplByName id) l ] -> (true,qid,l) ] ->
+	       l = OPT [ "["; l = LIST0 implicit_name; "]" -> 
+		   List.map (fun (id,b) -> (ExplByName id,b)) l ] ->
+		 (true,qid,l) ] ->
 	   VernacDeclareImplicits (local,qid,pos)
 
       | IDENT "Implicit"; ["Type" | IDENT "Types"];
 	   idl = LIST1 identref; ":"; c = lconstr -> VernacReserve (idl,c) ] ]
   ;
+  implicit_name:
+    [ [ id = ident -> (id,false) | "["; id = ident; "]" -> (id,true) ] ]
+  ;
 END
 
 GEXTEND Gram
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index e9d960e37c..7ccd8dd65d 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -146,9 +146,11 @@ let pr_search a b pr_p = match a with
 let pr_locality local = if local then str "Local " else str ""
 let pr_non_globality local = if local then str "" else str "Global "
 
-let pr_explanation imps = function
-  | ExplByPos n -> pr_id (Impargs.name_of_implicit (List.nth imps (n-1)))
-  | ExplByName id -> pr_id id
+let pr_explanation (e,b) =
+  let a = match e with
+  | ExplByPos n -> anomaly "No more supported"
+  | ExplByName id -> pr_id id in
+  if b then str "[" ++ a ++ str "]" else a
 
 let pr_class_rawexpr = function
   | FunClass -> str"Funclass"
@@ -753,13 +755,10 @@ let rec pr_vernac = function
          pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
   | VernacDeclareImplicits (local,q,None) ->
       hov 2 (str"Implicit Arguments" ++ spc() ++ pr_reference q)
-  | VernacDeclareImplicits (local,q,Some l) ->
-      let r = Nametab.global q in
-      Impargs.declare_manual_implicits local r l;
-      let imps = Impargs.implicits_of_global r in
+  | VernacDeclareImplicits (local,q,Some imps) ->
       hov 1 (str"Implicit Arguments" ++ pr_non_globality local ++
       spc() ++ pr_reference q ++ spc() ++
-             str"[" ++ prlist_with_sep sep (pr_explanation imps) l ++ str"]")
+             str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
   | VernacReserve (idl,c) ->
       hov 1 (str"Implicit Type" ++
         str (if List.length idl > 1 then "s " else " ") ++
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 64f6de12d2..4d311b177b 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -61,26 +61,24 @@ let print_closed_sections = ref false
 (********************************)
 (** Printing implicit arguments *)
 			  		  
-let print_impl_args_by_pos = function
-  | []  -> mt ()
-  | [i] -> str"Position [" ++ int i ++ str"] is implicit" ++ fnl()
-  | l   -> 
-      str"Positions [" ++ 
-      prlist_with_sep (fun () -> str "; ") int l ++
-      str"] are implicit" ++ fnl()
+let conjugate_to_be = function [_] -> "is" | _ -> "are"
+
+let pr_implicit imp = pr_id (name_of_implicit imp)
 
-let print_impl_args_by_name = function
+let print_impl_args_by_name max = 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()
+  | impls -> 
+      hov 0 (str (plural (List.length impls) "Argument") ++ spc() ++ 
+      prlist_with_sep pr_coma pr_implicit impls ++ spc() ++ 
+      str (conjugate_to_be impls) ++ str" implicit" ++
+      (if max then strbrk " and maximally inserted" else mt())) ++ fnl()
 
 let print_impl_args l = 
-  print_impl_args_by_name (List.filter is_status_implicit l)
+  let imps = List.filter is_status_implicit l in
+  let maximps = List.filter Impargs.maximal_insertion_of imps in
+  let nonmaximps = list_subtract imps maximps in
+  print_impl_args_by_name false nonmaximps ++
+  print_impl_args_by_name true maximps
 
 (*********************)
 (** Printing Scopes  *)