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

1 files changed, 7 insertions, 8 deletions

diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index e9d960e37..7ccd8dd65 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 " ") ++