diff options
Diffstat (limited to 'proofs/proof_trees.mli')
| -rw-r--r-- | proofs/proof_trees.mli | 14 |
1 files changed, 1 insertions, 13 deletions
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index 12f82b7f4..73a6bd9a8 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -43,16 +43,4 @@ val pf_lookup_index_as_renamed : env -> constr -> int -> int option open Pp (*i*) -val pr_goal : goal -> std_ppcmds -val pr_subgoals : goal list -> std_ppcmds -val pr_subgoal : int -> goal list -> std_ppcmds - -val pr_decl : goal -> std_ppcmds -val pr_decls : evar_map -> std_ppcmds -val pr_evc : named_context sigma -> std_ppcmds - -val prgl : goal -> std_ppcmds -val pr_seq : goal -> std_ppcmds -val pr_evars : (existential_key * goal) list -> std_ppcmds -val pr_evars_int : int -> (existential_key * goal) list -> std_ppcmds -val pr_subgoals_existential : evar_map -> goal list -> std_ppcmds +val db_pr_goal : goal -> std_ppcmds |