From c25e86e6b4e8bb694d3c8e50f04a92cc33ad807d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 24 Jul 2017 17:41:01 +0200
Subject: Turning the ltac2 subfolder into a standalone plugin.

---
 src/tac2print.mli | 37 +++++++++++++++++++++++++++++++++++++
 1 file changed, 37 insertions(+)
 create mode 100644 src/tac2print.mli

(limited to 'src/tac2print.mli')

diff --git a/src/tac2print.mli b/src/tac2print.mli
new file mode 100644
index 0000000000..ddd599641d
--- /dev/null
+++ b/src/tac2print.mli
@@ -0,0 +1,37 @@
+(************************************************************************)
+(*  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
+open Tac2expr
+
+(** {5 Printing types} *)
+
+type typ_level =
+| T5_l
+| T5_r
+| T2
+| T1
+| T0
+
+val pr_typref : type_constant -> std_ppcmds
+val pr_glbtype_gen : ('a -> string) -> typ_level -> 'a glb_typexpr -> std_ppcmds
+val pr_glbtype : ('a -> string) -> 'a glb_typexpr -> std_ppcmds
+
+(** {5 Printing expressions} *)
+
+val pr_constructor : ltac_constructor -> std_ppcmds
+val pr_projection : ltac_projection -> std_ppcmds
+val pr_glbexpr_gen : exp_level -> glb_tacexpr -> std_ppcmds
+val pr_glbexpr : glb_tacexpr -> std_ppcmds
+
+(** {5 Utilities} *)
+
+val int_name : unit -> (int -> string)
+(** Create a function that give names to integers. The names are generated on
+    the fly, in the order they are encountered. *)
-- 
cgit v1.2.3