diff options
| author | Hugo Herbelin | 2014-10-17 15:14:54 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-17 15:14:54 +0200 |
| commit | cfff8f8a32708ea0c8e72178424db0b40665fe37 (patch) | |
| tree | fe126ebb99be8e307df8a0a0f7837f51619a0eb8 /printing/printer.mli | |
| parent | bc8a5357889396f07d005a84bd3c50e9a25c1ddb (diff) | |
Experimental printing of the signature of open evars in Check.
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index bac864dc6a..315bf6810d 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -133,6 +133,7 @@ val pr_open_subgoals : ?proof:Proof.proof -> unit -> std_ppcmds val pr_nth_open_subgoal : int -> std_ppcmds val pr_evar : evar_map -> (evar * evar_info) -> std_ppcmds val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> std_ppcmds +val pr_evars : evar_map -> evar_info Evar.Map.t -> std_ppcmds val pr_prim_rule : prim_rule -> std_ppcmds |