diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-04 18:10:39 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-04 18:21:42 +0100 |
| commit | f8ee36d315f5359d92158407f830d10baeadf5b4 (patch) | |
| tree | 57545ed4740e75821a151ccfc6f40476f8492c7c /printing/printer.mli | |
| parent | 713b757cf4ca963fb9ab9f5f25eb263776f6abed (diff) | |
Improving error message when one instance-hole is not found.
Still to do:
- Decide between using SeveralInstancesFound or raising an error when
multiple instances exist.
- Use a proper printer for evars instead of the debugging
pr_evar_map_filter printer in pr_constraints.
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 ad6cedf7d..d41bff7bc 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -106,6 +106,7 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds (** Contexts *) +val pr_context_unlimited : env -> evar_map -> std_ppcmds val pr_ne_context_of : std_ppcmds -> env -> evar_map -> std_ppcmds val pr_var_decl : env -> evar_map -> named_declaration -> std_ppcmds |