1 files changed, 57 insertions, 0 deletions
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
new file mode 100644
index 0000000000..71e8150057
--- /dev/null
+++ b/src/tac2entries.mli
@@ -0,0 +1,57 @@
+(************************************************************************)
+(*  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 Names
+open Libnames
+open Tac2expr
+
+(** {5 Toplevel definitions} *)
+
+val register_ltac : ?local:bool -> rec_flag ->
+  (Name.t located * raw_tacexpr) list -> unit
+
+val register_type : ?local:bool -> rec_flag ->
+  (qualid located * redef_flag * raw_quant_typedef) list -> unit
+
+val register_primitive : ?local:bool ->
+  Id.t located -> raw_typexpr -> ml_tactic_name -> unit
+
+val register_struct : ?local:bool -> strexpr -> unit
+
+val register_notation : ?local:bool -> sexpr list -> int option ->
+  raw_tacexpr -> unit
+
+(** {5 Notations} *)
+
+type scope_rule =
+| ScopeRule : (raw_tacexpr, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule
+
+type scope_interpretation = sexpr list -> scope_rule
+
+val register_scope : Id.t -> scope_interpretation -> unit
+(** Create a new scope with the provided name *)
+
+val parse_scope : sexpr -> scope_rule
+(** Use this to interpret the subscopes for interpretation functions *)
+
+(** {5 Inspecting} *)
+
+val print_ltac : Libnames.reference -> unit
+
+(** {5 Eval loop} *)
+
+(** Evaluate a tactic expression in the current environment *)
+val call : default:bool -> raw_tacexpr -> unit
+
+(** {5 Parsing entries} *)
+
+module Pltac :
+sig
+val tac2expr : raw_tacexpr Pcoq.Gram.entry
+end