From f8ee36d315f5359d92158407f830d10baeadf5b4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 4 Dec 2014 18:10:39 +0100
Subject: 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.
---
 printing/printer.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index ad6cedf7dc..d41bff7bc1 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
-- 
cgit v1.2.3