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/tacentries.mli | 21 ++++++++++++---------
 1 file changed, 12 insertions(+), 9 deletions(-)

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

diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 3f804ee8..138a584e 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -12,10 +12,12 @@
 
 open Vernacexpr
 open Tacexpr
+open Vernacinterp
 
 (** {5 Tactic Definitions} *)
 
-val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit
+val register_ltac : locality_flag -> ?deprecation:deprecation ->
+  Tacexpr.tacdef_body list -> unit
 (** Adds new Ltac definitions to the environment. *)
 
 (** {5 Tactic Notations} *)
@@ -34,8 +36,8 @@ type argument = Genarg.ArgT.any Extend.user_symbol
     leaves. *)
 
 val add_tactic_notation :
-  locality_flag -> int -> raw_argument grammar_tactic_prod_item_expr list ->
-  raw_tactic_expr -> unit
+  locality_flag -> int -> ?deprecation:deprecation -> raw_argument
+  grammar_tactic_prod_item_expr list -> raw_tactic_expr -> unit
 (** [add_tactic_notation local level prods expr] adds a tactic notation in the
     environment at level [level] with locality [local] made of the grammar
     productions [prods] and returning the body [expr] *)
@@ -47,7 +49,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -
     to finding an argument by name (as in {!Genarg}) if there is none
     matching. *)
 
-val add_ml_tactic_notation : ml_tactic_name -> level:int ->
+val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:deprecation ->
   argument grammar_tactic_prod_item_expr list list -> unit
 (** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND
     ML-side macro. *)
@@ -55,7 +57,7 @@ val add_ml_tactic_notation : ml_tactic_name -> level:int ->
 (** {5 Tactic Quotations} *)
 
 val create_ltac_quotation : string ->
-  ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Gram.entry * int option) -> unit
+  ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Entry.t * int option) -> unit
 (** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is,
     Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and
     generates an argument using [f] on the entry parsed by [e]. *)
@@ -65,17 +67,18 @@ val create_ltac_quotation : string ->
 val print_ltacs : unit -> unit
 (** Display the list of ltac definitions currently available. *)
 
-val print_located_tactic : Libnames.reference -> unit
+val print_located_tactic : Libnames.qualid -> unit
 (** Display the absolute name of a tactic. *)
 
 type _ ty_sig =
 | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
 | TyIdent : string * 'r ty_sig -> 'r ty_sig
 | TyArg :
-  (('a, 'b, 'c) Extend.ty_user_symbol * Names.Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig
+  ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig
 | TyAnonArg :
-  ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig
+  ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig
 
 type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
 
-val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit
+val tactic_extend : string -> string -> level:Int.t ->
+  ?deprecation:deprecation -> ty_ml list -> unit
-- 
cgit v1.2.3