From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 contrib/subtac/subtac_utils.mli | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'contrib/subtac/subtac_utils.mli')

diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 4a7e8177..ebfc5123 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -10,6 +10,7 @@ open Rawterm
 open Util
 open Evarutil
 open Names
+open Sign
 
 val contrib_name : string
 val subtac_dir : string list
@@ -51,6 +52,7 @@ val my_print_constr : env -> constr -> std_ppcmds
 val my_print_constr_expr : constr_expr -> std_ppcmds
 val my_print_evardefs : evar_defs -> std_ppcmds
 val my_print_context : env -> std_ppcmds
+val my_print_named_context : env -> std_ppcmds
 val my_print_env : env -> std_ppcmds
 val my_print_rawconstr : env -> rawconstr -> std_ppcmds
 val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds
@@ -88,3 +90,11 @@ val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->
 val destruct_ex : constr -> constr -> constr list
 
 val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr
+val id_of_name : name -> identifier
+
+val definition_message : identifier -> unit
+val recursive_message : global_reference array -> std_ppcmds
+
+val solve_by_tac : evar_info -> Tacmach.tactic -> constr
+
+val string_of_list : string -> ('a -> string) -> 'a list -> string
-- 
cgit v1.2.3