From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- plugins/extraction/table.mli | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'plugins/extraction/table.mli') diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 2b163610..15a08756 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -21,8 +21,7 @@ val safe_basename_of_global : global_reference -> Id.t val warning_axioms : unit -> unit val warning_opaques : bool -> unit -val warning_both_mod_and_cst : - qualid -> module_path -> global_reference -> unit +val warning_ambiguous_name : ?loc:Loc.t -> qualid * module_path * global_reference -> unit val warning_id : string -> unit val error_axiom_scheme : global_reference -> int -> 'a val error_constant : global_reference -> 'a @@ -30,7 +29,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