From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 plugins/ltac/pptactic.mli | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/ltac/pptactic.mli')

diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 5951f2b1..6c09e447 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -14,11 +14,11 @@
 open Genarg
 open Geninterp
 open Names
-open Misctypes
 open Environ
 open Constrexpr
-open Notation_term
+open Notation_gram
 open Tacexpr
+open Tactypes
 
 type 'a grammar_tactic_prod_item_expr =
 | TacTerm of string
@@ -84,7 +84,7 @@ type pp_tactic = {
   pptac_prods : grammar_terminals;
 }
 
-val pr_goal_selector : toplevel:bool -> goal_selector -> Pp.t
+val pr_goal_selector : toplevel:bool -> Goal_select.t -> Pp.t
 
 val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
 
@@ -97,7 +97,7 @@ val pr_may_eval :
   ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) ->
   ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t
 
-val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t
+val pr_and_short_name : ('a -> Pp.t) -> 'a Stdarg.and_short_name -> Pp.t
 val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
 
 val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t
@@ -153,5 +153,5 @@ val pr_value : tolerability -> Val.t -> Pp.t
 
 val ltop : tolerability
 
-val make_constr_printer : (env -> Evd.evar_map -> Notation_term.tolerability -> 'a -> Pp.t) ->
+val make_constr_printer : (env -> Evd.evar_map -> tolerability -> 'a -> Pp.t) ->
   'a Genprint.top_printer
-- 
cgit v1.2.3