diff options
Diffstat (limited to 'contrib/subtac/subtac_utils.mli')
| -rw-r--r-- | contrib/subtac/subtac_utils.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index a53016484..92a995c89 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -47,6 +47,7 @@ val acc_inv : constr lazy_t val extconstr : constr -> constr_expr val extsort : sorts -> constr_expr 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_env : env -> std_ppcmds |