diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-24 11:54:00 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-24 20:09:01 +0100 |
| commit | ef61bb05911d19c77d565d78dc57107d40c333e4 (patch) | |
| tree | be7f3694bbd0f5c6d31b931471a70059a9c4af3d /printing/printer.mli | |
| parent | f4d77142a6e1d298fadf4219c46fcc9ff8abe62a (diff) | |
Isolate a function for printing evar sets.
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index 6b9c70815..42ed2b6d9 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -137,6 +137,8 @@ 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_ne_evar_set : std_ppcmds -> std_ppcmds -> evar_map -> + Evar.Set.t -> std_ppcmds val pr_prim_rule : prim_rule -> std_ppcmds |