From 956eab0d8af124ef30cb4319f3798f6776919eca Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 6 May 2007 13:00:39 +0000 Subject: Nouveaux changements autour des implicites (notamment suite à discussion avec Georges) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - 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 --- parsing/ppvernac.ml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) (limited to 'parsing/ppvernac.ml') 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 " ") ++ -- cgit v1.2.3