diff options
Diffstat (limited to 'plugins/subtac/subtac_utils.mli')
| -rw-r--r-- | plugins/subtac/subtac_utils.mli | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli index f56c2932..de96cc60 100644 --- a/plugins/subtac/subtac_utils.mli +++ b/plugins/subtac/subtac_utils.mli @@ -6,7 +6,7 @@ open Pp open Evd open Decl_kinds open Topconstr -open Rawterm +open Glob_term open Util open Evarutil open Names @@ -15,11 +15,9 @@ open Sign val ($) : ('a -> 'b) -> 'a -> 'b val contrib_name : string val subtac_dir : string list -val fix_sub_module : string val fixsub_module : string list val init_constant : string list -> string -> constr delayed val init_reference : string list -> string -> global_reference delayed -val fixsub : constr delayed val well_founded_ref : global_reference delayed val acc_ref : global_reference delayed val acc_inv_ref : global_reference delayed @@ -35,7 +33,8 @@ val build_sig : unit -> coq_sigma_data val sig_ : coq_sigma_data delayed val fix_proto : constr delayed -val fix_proto_ref : unit -> constant + +val hide_obligation : constr delayed val eq_ind : constr delayed val eq_rec : constr delayed @@ -52,11 +51,6 @@ val jmeq_ind : constr delayed val jmeq_rec : constr delayed val jmeq_refl : constr delayed -val boolind : constr delayed -val sumboolind : constr delayed -val natind : constr delayed -val intind : constr delayed -val existSind : constr delayed val existS : coq_sigma_data delayed val prod : coq_sigma_data delayed @@ -74,7 +68,7 @@ val my_print_context : env -> std_ppcmds val my_print_rel_context : env -> rel_context -> 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_glob_constr : env -> glob_constr -> std_ppcmds val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds |