diff options
author | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
commit | 3e96002677226c0cdaa8f355938a76cfb37a722a (patch) | |
tree | 3ca96e142fdb68e464d2f5f403f315282b94f922 /parsing/ppvernac.ml | |
parent | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff) |
Imported Upstream version 8.3upstream/8.3
Diffstat (limited to 'parsing/ppvernac.ml')
-rw-r--r-- | parsing/ppvernac.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index ff35be57..b5e0cc4a 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: ppvernac.ml 13332 2010-07-26 22:12:43Z msozeau $ *) +(* $Id: ppvernac.ml 13492 2010-10-04 21:20:01Z herbelin $ *) open Pp open Names @@ -847,13 +847,15 @@ let rec pr_vernac = function (pr_locality local ++ str"Notation " ++ pr_lident id ++ prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++ pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else [])) - | VernacDeclareImplicits (local,q,None) -> + | VernacDeclareImplicits (local,q,[]) -> hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++ pr_smart_global q) - | VernacDeclareImplicits (local,q,Some imps) -> + | VernacDeclareImplicits (local,q,impls) -> hov 1 (pr_section_locality local ++ str"Implicit Arguments " ++ spc() ++ pr_smart_global q ++ spc() ++ - str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") + prlist_with_sep spc (fun imps -> + str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]") + impls) | VernacReserve bl -> let n = List.length (List.flatten (List.map fst bl)) in hov 2 (str"Implicit Type" ++ |