diff options
Diffstat (limited to 'contrib/subtac/subtac_utils.mli')
| -rw-r--r-- | contrib/subtac/subtac_utils.mli | 10 |
1 files changed, 10 insertions, 0 deletions
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 |