6 files changed, 15 insertions, 20 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 608b778e4f..799e969ae2 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open Grammar_API
 open Util
 open Names
 open Evd
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 4b045e989a..2eadd5f26c 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -41,7 +41,7 @@ val nohint : 'a ssrhint
 
 (******************************** misc ************************************)
 
-val errorstrm : Pp.std_ppcmds -> 'a
+val errorstrm : Pp.t -> 'a
 val anomaly : string -> 'a
 
 val array_app_tl : 'a array -> 'a list -> 'a list
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 228444b82e..ce23bb2b30 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open Grammar_API
 open Names
 open Pp
 open Pcoq
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index c93e104056..88beeaa711 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -8,8 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open Grammar_API
-
 val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
 val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
 val pr_ssrtacarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c) -> 'c
@@ -18,5 +16,5 @@ val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
 val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
 val pr_ssrtclarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c -> 'd) -> 'c -> 'd
 
-val add_genarg : string -> ('a -> Pp.std_ppcmds) -> 'a Genarg.uniform_genarg_type
+val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type
 
diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli
index 5c68872b75..f231068265 100644
--- a/plugins/ssr/ssrprinters.mli
+++ b/plugins/ssr/ssrprinters.mli
@@ -11,16 +11,16 @@
 open Ssrast
 
 val pp_term :
-  Goal.goal Evd.sigma -> EConstr.constr -> Pp.std_ppcmds
+  Goal.goal Evd.sigma -> EConstr.constr -> Pp.t
 
-val pr_spc : unit -> Pp.std_ppcmds
-val pr_bar : unit -> Pp.std_ppcmds
+val pr_spc : unit -> Pp.t
+val pr_bar : unit -> Pp.t
 val pr_list : 
-  (unit -> Pp.std_ppcmds) -> ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds
+  (unit -> Pp.t) -> ('a -> Pp.t) -> 'a list -> Pp.t
 
 val pp_concat :
-  Pp.std_ppcmds ->
-  ?sep:Pp.std_ppcmds -> Pp.std_ppcmds list -> Pp.std_ppcmds
+  Pp.t ->
+  ?sep:Pp.t -> Pp.t list -> Pp.t
 
 val xInParens : ssrtermkind
 val xWithAt : ssrtermkind
@@ -29,17 +29,17 @@ val xCpattern : ssrtermkind
 
 val pr_term :
   ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option) ->
-  Pp.std_ppcmds
+  Pp.t
 
-val pr_hyp : ssrhyp -> Pp.std_ppcmds
+val pr_hyp : ssrhyp -> Pp.t
 
-val prl_constr_expr : Constrexpr.constr_expr -> Pp.std_ppcmds
-val prl_glob_constr : Glob_term.glob_constr -> Pp.std_ppcmds
+val prl_constr_expr : Constrexpr.constr_expr -> Pp.t
+val prl_glob_constr : Glob_term.glob_constr -> Pp.t
 
 val pr_guarded :
-  (string -> int -> bool) -> ('a -> Pp.std_ppcmds) -> 'a -> Pp.std_ppcmds
+  (string -> int -> bool) -> ('a -> Pp.t) -> 'a -> Pp.t
 
-val pr_occ : ssrocc -> Pp.std_ppcmds
+val pr_occ : ssrocc -> Pp.t
 
-val ppdebug : Pp.std_ppcmds Lazy.t -> unit
+val ppdebug : Pp.t Lazy.t -> unit
 
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index fbe3cd2b91..9c59d83d4e 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open Grammar_API
 open Names
 open Term
 open Termops