Extraction: nicer implementation of Implicits

 Instead of the original hacks (embedding implicits in string msg in MLexn !)
 we now use a proper construction MLdummy (Kimplicit (r,i)) to replace the use
 of the i-th argument of constant or constructor r when this argument has been
 declared as implicit.

 A new option Set/Unset Extraction SafeImplicits controls what happens
 when some implicits still occur after an extraction : fail in safe mode,
 or otherwise produce some code nonetheless. This code is probably buggish
 if the implicits are actually used to do anything relevant (match, function
 call, etc), but it might also be fine if the implicits are just passed along.
 And anyway, this unsafe mode could help figure what's going on.

 Note: the MLdummy now expected a kill_reason, just as Tdummy.
 These kill_reason are now Ktype, Kprop (formerly Kother) and Kimplicit.

 Some minor refactoring on the fly.

1 files changed, 3 insertions, 3 deletions

diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 648f23211..a6734dae8 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -38,8 +38,8 @@ val error_MPfile_as_mod : module_path -> bool -> 'a
 val check_inside_module : unit -> unit
 val check_inside_section : unit -> unit
 val check_loaded_modfile : module_path -> unit
-val msg_non_implicit : global_reference -> int -> Name.t -> string
-val error_non_implicit : string -> 'a
+val msg_of_implicit : kill_reason -> string
+val err_or_warn_remaining_implicit : kill_reason -> unit
 
 val info_file : string -> unit
 
@@ -166,7 +166,7 @@ val to_keep : global_reference -> bool
 
 (*s Table for implicits arguments *)
 
-val implicits_of_global : global_reference -> int list
+val implicits_of_global : global_reference -> Int.Set.t
 
 (*s Table for user-given custom ML extractions. *)