diff options
| author | Hugo Herbelin | 2015-10-31 15:49:09 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-11-02 15:46:40 +0100 |
| commit | 4e643d134f02cfa9a73754c3cf48048541324834 (patch) | |
| tree | 54a8d34fb69fd23b1d5034f13c2cafb20fcc3e0f /printing/printer.mli | |
| parent | 69be6a29cf9f774cb4afe94d76b157ba50984c1d (diff) | |
Adding syntax "Show id" to show goal named id (shelved or not).
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index 0a44e4f103..5c60b89366 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -176,7 +176,8 @@ module ContextObjectMap : CMap.ExtS val pr_assumptionset : env -> Term.types ContextObjectMap.t -> std_ppcmds -val pr_goal_by_id : string -> std_ppcmds +val pr_goal_by_id : Id.t -> std_ppcmds +val pr_goal_by_uid : string -> std_ppcmds type printer_pr = { pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; |