Merge branch 'trunk' into pr379

14 files changed, 178 insertions, 395 deletions

diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index 7b2c5695f..360843711 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -28,7 +28,7 @@ and pr_intro_pattern_action prc = function
   | IntroInjection pl ->
       str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++
       str "]"
-  | IntroApplyOn (c,pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c
+  | IntroApplyOn ((_,c),pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c
   | IntroRewrite true -> str "->"
   | IntroRewrite false -> str "<-"
 
diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
deleted file mode 100644
index 726c0ffcf..000000000
--- a/printing/ppannotation.ml
+++ /dev/null
@@ -1,33 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Ppextend
-open Constrexpr
-open Vernacexpr
-open Genarg
-
-type t =
-  | AKeyword
-  | AUnparsing            of unparsing
-  | AConstrExpr           of constr_expr
-  | AVernac               of vernac_expr
-  | AGlbGenArg            of glob_generic_argument
-  | ARawGenArg            of raw_generic_argument
-
-let tag_of_annotation = function
-  | AKeyword                -> "keyword"
-  | AUnparsing _            -> "unparsing"
-  | AConstrExpr _           -> "constr_expr"
-  | AVernac _               -> "vernac_expr"
-  | AGlbGenArg _            -> "glob_generic_argument"
-  | ARawGenArg _            -> "raw_generic_argument"
-
-let attributes_of_annotation a =
-  []
-
-let tag = Pp.Tag.create "ppannotation"
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli
deleted file mode 100644
index b0e0facef..000000000
--- a/printing/ppannotation.mli
+++ /dev/null
@@ -1,29 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** This module defines the annotations that are attached to
-    semi-structured pretty-printing of Coq syntactic objects. *)
-
-open Ppextend
-open Constrexpr
-open Vernacexpr
-open Genarg
-
-type t =
-  | AKeyword
-  | AUnparsing            of unparsing
-  | AConstrExpr           of constr_expr
-  | AVernac               of vernac_expr
-  | AGlbGenArg            of glob_generic_argument
-  | ARawGenArg            of raw_generic_argument
-
-val tag_of_annotation : t -> string
-
-val attributes_of_annotation : t -> (string * string) list
-
-val tag : t Pp.Tag.key
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 80ddd669f..d92d83275 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -21,18 +21,31 @@ open Decl_kinds
 open Misctypes
 (*i*)
 
-module Make (Taggers : sig
-  val tag_keyword     : std_ppcmds -> std_ppcmds
-  val tag_evar     : std_ppcmds -> std_ppcmds
-  val tag_type     : std_ppcmds -> std_ppcmds
-  val tag_path     : std_ppcmds -> std_ppcmds
-  val tag_ref     : std_ppcmds -> std_ppcmds
-  val tag_var     : std_ppcmds -> std_ppcmds
-  val tag_constr_expr : constr_expr -> std_ppcmds -> std_ppcmds
-  val tag_unparsing   : unparsing -> std_ppcmds -> std_ppcmds
-end) = struct
-
-  open Taggers
+module Tag =
+struct
+  let keyword   = "constr.keyword"
+  let evar      = "constr.evar"
+  let univ      = "constr.type"
+  let notation  = "constr.notation"
+  let variable  = "constr.variable"
+  let reference = "constr.reference"
+  let path      = "constr.path"
+
+end
+
+let do_not_tag _ x = x
+let tag t s = Pp.tag t s
+let tag_keyword     = tag Tag.keyword
+let tag_evar        = tag Tag.evar
+let tag_type        = tag Tag.univ
+let tag_unparsing   = function
+| UnpTerminal s -> tag Tag.notation
+| _ -> do_not_tag ()
+let tag_constr_expr = do_not_tag
+let tag_path = tag Tag.path
+let tag_ref = tag Tag.reference
+let tag_var = tag Tag.variable
+
 
   let keyword s = tag_keyword (str s)
   let sep_v = fun _ -> str"," ++ spc()
@@ -764,86 +777,3 @@ end) = struct
 
   let pr_binders = pr_undelimited_binders spc (pr ltop)
 
-end
-
-module Tag =
-struct
-  let keyword =
-    let style = Terminal.make ~bold:true () in
-    Ppstyle.make ~style ["constr"; "keyword"]
-
-  let evar =
-    let style = Terminal.make ~fg_color:`LIGHT_BLUE () in
-    Ppstyle.make ~style ["constr"; "evar"]
-
-  let univ =
-    let style = Terminal.make ~bold:true ~fg_color:`YELLOW () in
-    Ppstyle.make ~style ["constr"; "type"]
-
-  let notation =
-    let style = Terminal.make ~fg_color:`WHITE () in
-    Ppstyle.make ~style ["constr"; "notation"]
-
-  let variable =
-    Ppstyle.make ["constr"; "variable"]
-
-  let reference =
-    let style = Terminal.make ~fg_color:`LIGHT_GREEN () in
-    Ppstyle.make ~style ["constr"; "reference"]
-
-  let path =
-    let style = Terminal.make ~fg_color:`LIGHT_MAGENTA () in
-    Ppstyle.make ~style ["constr"; "path"]
-
-end
-
-let do_not_tag _ x = x
-
-let split_token tag s =
-  let len = String.length s in
-  let rec parse_string off i =
-    if Int.equal i len then
-      if Int.equal off i then mt () else tag (str (String.sub s off (i - off)))
-    else if s.[i] == ' ' then
-      if Int.equal off i then parse_space 1 (succ i)
-      else tag (str (String.sub s off (i - off))) ++ parse_space 1 (succ i)
-    else parse_string off (succ i)
-  and parse_space spc i =
-    if Int.equal i len then str (String.make spc ' ')
-    else if s.[i] == ' ' then parse_space (succ spc) (succ i)
-    else str (String.make spc ' ') ++ parse_string i (succ i)
-  in
-  parse_string 0 0
-
-(** Instantiating Make with tagging functions that only add style
-    information. *)
-include Make (struct
-    let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
-    let tag_keyword     = tag Tag.keyword
-    let tag_evar        = tag Tag.evar
-    let tag_type        = tag Tag.univ
-    let tag_unparsing   = function
-    | UnpTerminal s -> fun _ -> split_token (fun pp -> tag Tag.notation pp) s
-    | _ -> do_not_tag ()
-    let tag_constr_expr = do_not_tag
-    let tag_path = tag Tag.path
-    let tag_ref = tag Tag.reference
-    let tag_var = tag Tag.variable
-end)
-
-module Richpp = struct
-
-  include Make (struct
-    open Ppannotation
-    let tag_keyword       = Pp.tag (Pp.Tag.inj AKeyword tag)
-    let tag_type          = Pp.tag (Pp.Tag.inj AKeyword tag)
-    let tag_evar          = do_not_tag ()
-    let tag_unparsing unp = Pp.tag (Pp.Tag.inj (AUnparsing unp) tag)
-    let tag_constr_expr e = Pp.tag (Pp.Tag.inj (AConstrExpr e) tag)
-    let tag_path = do_not_tag ()
-    let tag_ref = do_not_tag ()
-    let tag_var = do_not_tag ()
-  end)
-
-end
-
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 0241633c6..a0106837a 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -11,11 +11,85 @@
 
 (** The default pretty-printers produce {!Pp.std_ppcmds} that are
     interpreted as raw strings. *)
-include Ppconstrsig.Pp
+open Loc
+open Pp
+open Libnames
+open Constrexpr
+open Names
+open Misctypes
 
-(** The rich pretty-printers produce {!Pp.std_ppcmds} that are
-    interpreted as annotated strings. The annotations can be
-    retrieved using {!RichPp.rich_pp}. Their definitions are
-    located in {!Ppannotation.t}. *)
+val extract_lam_binders :
+  constr_expr -> local_binder list * constr_expr
+val extract_prod_binders :
+  constr_expr -> local_binder list * constr_expr
+val split_fix :
+  int -> constr_expr -> constr_expr ->
+  local_binder list *  constr_expr * constr_expr
 
-module Richpp : Ppconstrsig.Pp
+val prec_less : int -> int * Ppextend.parenRelation -> bool
+
+val pr_tight_coma : unit -> std_ppcmds
+
+val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
+
+val pr_lident : Id.t located -> std_ppcmds
+val pr_lname : Name.t located -> std_ppcmds
+
+val pr_with_comments : Loc.t -> std_ppcmds -> std_ppcmds
+val pr_com_at : int -> std_ppcmds
+val pr_sep_com :
+  (unit -> std_ppcmds) ->
+  (constr_expr -> std_ppcmds) ->
+  constr_expr -> std_ppcmds
+
+val pr_id : Id.t -> std_ppcmds
+val pr_name : Name.t -> std_ppcmds
+val pr_qualid : qualid -> std_ppcmds
+val pr_patvar : patvar -> std_ppcmds
+
+val pr_glob_level : glob_level -> std_ppcmds
+val pr_glob_sort : glob_sort -> std_ppcmds
+val pr_guard_annot : (constr_expr -> std_ppcmds) ->
+  local_binder list ->
+  ('a * Names.Id.t) option * recursion_order_expr ->
+  std_ppcmds
+
+val pr_record_body : (reference * constr_expr) list -> std_ppcmds
+val pr_binders : local_binder list -> std_ppcmds
+val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
+val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
+val pr_constr_expr : constr_expr -> std_ppcmds
+val pr_lconstr_expr : constr_expr -> std_ppcmds
+val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
+
+type term_pr = {
+  pr_constr_expr   : constr_expr -> std_ppcmds;
+  pr_lconstr_expr  : constr_expr -> std_ppcmds;
+  pr_constr_pattern_expr  : constr_pattern_expr -> std_ppcmds;
+  pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
+}
+
+val set_term_pr : term_pr -> unit
+val default_term_pr : term_pr
+
+(* The modular constr printer.
+  [modular_constr_pr pr s p t] prints the head of the term [t] and calls
+  [pr] on its subterms.
+  [s] is typically {!Pp.mt} and [p] is [lsimpleconstr] for "constr" printers
+  and [ltop] for "lconstr" printers (spiwack: we might need more
+  specification here).
+  We can make a new modular constr printer by overriding certain branches,
+  for instance if we want to build a printer which prints "Prop" as "Omega"
+  instead we can proceed as follows:
+  let my_modular_constr_pr pr s p = function
+  | CSort (_,GProp Null) -> str "Omega"
+  | t -> modular_constr_pr pr s p t
+  Which has the same type. We can turn a modular printer into a printer by
+  taking its fixpoint. *)
+
+type precedence
+val lsimpleconstr : precedence
+val ltop : precedence
+val modular_constr_pr :
+  ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) ->
+  (unit->std_ppcmds) -> precedence  -> constr_expr -> std_ppcmds
diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli
deleted file mode 100644
index 3de0d805c..000000000
--- a/printing/ppconstrsig.mli
+++ /dev/null
@@ -1,95 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Loc
-open Pp
-open Libnames
-open Constrexpr
-open Names
-open Misctypes
-
-module type Pp = sig
-
-  val extract_lam_binders :
-    constr_expr -> local_binder list * constr_expr
-  val extract_prod_binders :
-    constr_expr -> local_binder list * constr_expr
-  val split_fix :
-    int -> constr_expr -> constr_expr ->
-    local_binder list *  constr_expr * constr_expr
-
-  val prec_less : int -> int * Ppextend.parenRelation -> bool
-
-  val pr_tight_coma : unit -> std_ppcmds
-
-  val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
-
-  val pr_lident : Id.t located -> std_ppcmds
-  val pr_lname : Name.t located -> std_ppcmds
-
-  val pr_with_comments : Loc.t -> std_ppcmds -> std_ppcmds
-  val pr_com_at : int -> std_ppcmds
-  val pr_sep_com :
-    (unit -> std_ppcmds) ->
-    (constr_expr -> std_ppcmds) ->
-    constr_expr -> std_ppcmds
-
-  val pr_id : Id.t -> std_ppcmds
-  val pr_name : Name.t -> std_ppcmds
-  val pr_qualid : qualid -> std_ppcmds
-  val pr_patvar : patvar -> std_ppcmds
-
-  val pr_glob_level : glob_level -> std_ppcmds
-  val pr_glob_sort : glob_sort -> std_ppcmds
-  val pr_guard_annot : (constr_expr -> std_ppcmds) ->
-    local_binder list ->
-    ('a * Names.Id.t) option * recursion_order_expr ->
-    std_ppcmds
-
-  val pr_record_body : (reference * constr_expr) list -> std_ppcmds
-  val pr_binders : local_binder list -> std_ppcmds
-  val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
-  val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
-  val pr_constr_expr : constr_expr -> std_ppcmds
-  val pr_lconstr_expr : constr_expr -> std_ppcmds
-  val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
-
-  type term_pr = {
-    pr_constr_expr   : constr_expr -> std_ppcmds;
-    pr_lconstr_expr  : constr_expr -> std_ppcmds;
-    pr_constr_pattern_expr  : constr_pattern_expr -> std_ppcmds;
-    pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
-  }
-
-  val set_term_pr : term_pr -> unit
-  val default_term_pr : term_pr
-
-(** The modular constr printer.
-    [modular_constr_pr pr s p t] prints the head of the term [t] and calls
-    [pr] on its subterms.
-    [s] is typically {!Pp.mt} and [p] is [lsimpleconstr] for "constr" printers
-    and [ltop] for "lconstr" printers (spiwack: we might need more
-    specification here).
-    We can make a new modular constr printer by overriding certain branches,
-    for instance if we want to build a printer which prints "Prop" as "Omega"
-    instead we can proceed as follows:
-    let my_modular_constr_pr pr s p = function
-    | CSort (_,GProp Null) -> str "Omega"
-    | t -> modular_constr_pr pr s p t
-    Which has the same type. We can turn a modular printer into a printer by
-    taking its fixpoint. *)
-
-  type precedence
-  val lsimpleconstr : precedence
-  val ltop : precedence
-  val modular_constr_pr :
-    ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) ->
-    (unit->std_ppcmds) -> precedence  -> constr_expr -> std_ppcmds
-
-end
-
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index ff72be90c..78ef4d4ba 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -19,17 +19,12 @@ open Constrexpr
 open Constrexpr_ops
 open Decl_kinds
 
-module Make
-  (Ppconstr : Ppconstrsig.Pp)
-  (Taggers  : sig
-    val tag_keyword : std_ppcmds -> std_ppcmds
-    val tag_vernac  : vernac_expr -> std_ppcmds -> std_ppcmds
-  end)
-= struct
-
-  open Taggers
   open Ppconstr
 
+  let do_not_tag _ x = x
+  let tag_keyword = do_not_tag ()
+  let tag_vernac  = do_not_tag
+
   let keyword s = tag_keyword (str s)
 
   let pr_constr = pr_constr_expr
@@ -526,7 +521,7 @@ module Make
   let pr_using e = str (Proof_using.to_string e)
 
   let rec pr_vernac_body v =
-    let return = Taggers.tag_vernac v in
+    let return = tag_vernac v in
     match v with
       | VernacPolymorphic (poly, v) ->
         let s = if poly then keyword "Polymorphic" else keyword "Monomorphic" in
@@ -1244,23 +1239,3 @@ module Make
   let pr_vernac v =
     try pr_vernac_body v ++ sep_end v
     with e -> CErrors.print e
-
-end
-
-include Make (Ppconstr) (struct
-  let do_not_tag _ x = x
-  let tag_keyword = do_not_tag ()
-  let tag_vernac  = do_not_tag
-end)
-
-module Richpp = struct
-
-  include Make
-    (Ppconstr.Richpp)
-    (struct
-      open Ppannotation
-      let tag_keyword s = Pp.tag (Pp.Tag.inj AKeyword tag) s
-      let tag_vernac v s = Pp.tag (Pp.Tag.inj (AVernac v) tag) s
-     end)
-
-end
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index d3d4a5ceb..836b05e0e 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -9,12 +9,11 @@
 (** This module implements pretty-printers for vernac_expr syntactic
     objects and their subcomponents. *)
 
-(** The default pretty-printers produce {!Pp.std_ppcmds} that are
-    interpreted as raw strings. *)
-include Ppvernacsig.Pp
+(** Prints a fixpoint body *)
+val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds
 
-(** The rich pretty-printers produce {!Pp.std_ppcmds} that are
-    interpreted as annotated strings. The annotations can be
-    retrieved using {!RichPp.rich_pp}. Their definitions are
-    located in {!Ppannotation.t}. *)
-module Richpp : Ppvernacsig.Pp
+(** Prints a vernac expression *)
+val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds
+
+(** Prints a vernac expression and closes it with a dot. *)
+val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds
diff --git a/printing/ppvernacsig.mli b/printing/ppvernacsig.mli
deleted file mode 100644
index 5e5e4bcf4..000000000
--- a/printing/ppvernacsig.mli
+++ /dev/null
@@ -1,20 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-module type Pp = sig
-
-  (** Prints a fixpoint body *)
-  val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds
-
-  (** Prints a vernac expression *)
-  val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds
-
-  (** Prints a vernac expression and closes it with a dot. *)
-  val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds
-
-end
diff --git a/printing/printer.ml b/printing/printer.ml
index f05968383..239e1d7eb 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -306,6 +306,9 @@ let pr_named_context_of env sigma =
   let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in
   hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
 
+let pr_var_list_decl env sigma decl =
+  hov 0 (pr_compacted_decl env sigma decl)
+
 let pr_named_context env sigma ne_context =
   hv 0 (Context.Named.fold_outside
 	  (fun d pps -> pps ++ ws 2 ++ pr_named_decl env sigma d)
@@ -339,39 +342,43 @@ let pr_ne_context_of header env sigma =
     List.is_empty (Environ.named_context env)  then (mt ())
   else let penv = pr_context_unlimited env sigma in (header ++ penv ++ fnl ())
 
-let pr_context_limit n env sigma =
-  let named_context = Environ.named_context env in
-  let lgsign = List.length named_context in
-  if n >= lgsign then
-    pr_context_unlimited env sigma
-  else
-    let k = lgsign-n in
-    let _,sign_env =
-      Context.Compacted.fold
-        (fun d (i,pps) ->
-           if i < k then
-	     (i+1, (pps ++str "."))
-	   else
-             let pidt = pr_compacted_decl env sigma d in
-	     (i+1, (pps ++ fnl () ++
-		      str (emacs_str "") ++
-		      pidt)))
-        (Termops.compact_named_context (Environ.named_context env)) ~init:(0,(mt ()))
-    in
-    let db_env =
-      fold_rel_context
-        (fun env d pps ->
-           let pnat = pr_rel_decl env sigma d in
-	   (pps ++ fnl () ++
-	      str (emacs_str "") ++
-	      pnat))
-        env ~init:(mt ())
-    in
-    (sign_env ++ db_env)
+let rec bld_sign_env env sigma ctxt pps =
+  match ctxt with
+  | [] -> pps
+  | d:: ctxt' ->
+     let pidt = pr_var_list_decl env sigma d in
+     let pps' = pps ++ brk (0,0) ++ pidt in
+     bld_sign_env env sigma ctxt' pps'
+
+
+let pr_context_limit_compact ?n env sigma =
+  let ctxt = Termops.compact_named_context (named_context env) in
+  let lgth = List.length ctxt in
+  let n_capped =
+    match n with
+    | None -> lgth
+    | Some n when n > lgth -> lgth
+    | Some n -> n in
+  let ctxt_chopped,ctxt_hidden = Util.List.chop n_capped ctxt in
+  (* a dot line hinting the number of hiden hyps. *)
+  let hidden_dots = String.make (List.length ctxt_hidden) '.' in
+  let sign_env = v 0 (str hidden_dots ++ (mt ())
+                 ++ bld_sign_env env sigma (List.rev ctxt_chopped) (mt ())) in
+  let db_env =
+    fold_rel_context
+      (fun env d pps -> pps ++ fnl () ++ pr_rel_decl env sigma d)
+      env ~init:(mt ()) in
+  (sign_env ++ db_env)
+
+(* compact printing an env (variables and de Bruijn). Separator: three
+   spaces between simple hyps, and newline otherwise *)
+let pr_context_unlimited_compact env sigma =
+  pr_context_limit_compact env sigma
 
-let pr_context_of env sigma = match Flags.print_hyps_limit () with
-  | None -> hv 0 (pr_context_unlimited env sigma)
-  | Some n -> hv 0 (pr_context_limit n env sigma)
+let pr_context_of env sigma =
+  match Flags.print_hyps_limit () with
+  | None -> hv 0 (pr_context_limit_compact env sigma)
+  | Some n -> hv 0 (pr_context_limit_compact ~n env sigma)
 
 (* display goal parts (Proof mode) *)
 
@@ -725,7 +732,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
             let end_cmd =
               str "This subproof is complete, but there are some unfocused goals." ++
               (let s = Proof_global.Bullet.suggest p in
-               if Pp.is_empty s then s else fnl () ++ s) ++
+               if Pp.ismt s then s else fnl () ++ s) ++
               fnl ()
             in
 	    pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals
diff --git a/printing/printing.mllib b/printing/printing.mllib
index b0141b6d3..86b68d8fb 100644
--- a/printing/printing.mllib
+++ b/printing/printing.mllib
@@ -1,6 +1,5 @@
 Genprint
 Pputils
-Ppannotation
 Ppconstr
 Printer
 Printmod
diff --git a/printing/printmod.ml b/printing/printmod.ml
index e8ea0a99a..6f4b162d7 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -26,6 +26,18 @@ open Goptions
     the "short" mode or (Some env) in the "rich" one.
 *)
 
+module Tag =
+struct
+
+  let definition = "module.definition"
+  let keyword    = "module.keyword"
+
+end
+
+let tag t s = Pp.tag t s
+let tag_definition s = tag Tag.definition s
+let tag_keyword s = tag Tag.keyword s
+
 let short = ref false
 
 let _ =
@@ -44,14 +56,8 @@ let mk_fake_top =
   let r = ref 0 in
   fun () -> incr r; Id.of_string ("FAKETOP"^(string_of_int !r))
 
-module Make (Taggers : sig
-  val tag_definition : std_ppcmds -> std_ppcmds
-  val tag_keyword : std_ppcmds -> std_ppcmds
-end) =
-struct
-
-let def s = Taggers.tag_definition (str s)
-let keyword s = Taggers.tag_keyword (str s)
+let def s = tag_definition (str s)
+let keyword s = tag_keyword (str s)
 
 let get_new_id locals id =
   let rec get_id l id =
@@ -397,11 +403,11 @@ let rec printable_body dir =
 
 let print_expression' is_type env mp me =
   States.with_state_protection
-    (fun e -> eval_ppcmds (print_expression is_type env mp [] e)) me
+    (fun e -> print_expression is_type env mp [] e) me
 
 let print_signature' is_type env mp me =
   States.with_state_protection
-    (fun e -> eval_ppcmds (print_signature is_type env mp [] e)) me
+    (fun e -> print_signature is_type env mp [] e) me
 
 let unsafe_print_module env mp with_body mb =
   let name = print_modpath [] mp in
@@ -441,20 +447,4 @@ let print_modtype kn =
       with e when CErrors.noncritical e ->
 	print_signature' true None kn mtb.mod_type))
 
-end
-
-module Tag =
-struct
-  let definition =
-    let style = Terminal.make ~bold:true ~fg_color:`LIGHT_RED () in
-    Ppstyle.make ~style ["module"; "definition"]
-  let keyword =
-    let style = Terminal.make ~bold:true () in
-    Ppstyle.make ~style ["module"; "keyword"]
-end
 
-include Make(struct
-  let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
-  let tag_definition s = tag Tag.definition s
-  let tag_keyword s = tag Tag.keyword s
-end)
diff --git a/printing/printmod.mli b/printing/printmod.mli
index 7f7d34392..f3079d5b6 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -6,9 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
 open Names
 
 (** false iff the module is an element of an open module type *)
 val printable_body : DirPath.t -> bool
 
-include Printmodsig.Pp
+val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds
+val print_module : bool -> module_path -> std_ppcmds
+val print_modtype : module_path -> std_ppcmds
diff --git a/printing/printmodsig.mli b/printing/printmodsig.mli
deleted file mode 100644
index f71fffdce..000000000
--- a/printing/printmodsig.mli
+++ /dev/null
@@ -1,17 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Pp
-open Names
-
-module type Pp =
-sig
-  val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds
-  val print_module : bool -> module_path -> std_ppcmds
-  val print_modtype : module_path -> std_ppcmds
-end