From cb31cd671a0ef4da0cf834dad5b67776098bb0d1 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 30 May 2016 17:16:25 +0200
Subject: Extraction : add a location in the error message about polyprop

---
 plugins/extraction/table.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/extraction/table.mli')

diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 2b163610e9..62c20bd3a7 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -30,7 +30,7 @@ val error_inductive : global_reference -> 'a
 val error_nb_cons : unit -> 'a
 val error_module_clash : module_path -> module_path -> 'a
 val error_no_module_expr : module_path -> 'a
-val error_singleton_become_prop : Id.t -> 'a
+val error_singleton_become_prop : Id.t -> global_reference option -> 'a
 val error_unknown_module : qualid -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a
-- 
cgit v1.2.3