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.

12 files changed, 166 insertions, 138 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 1d7f61456..3d32398ff 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -498,8 +498,8 @@ let print_structure_to_file (fn,si,mo) dry struc =
   let d = descr () in
   reset_renaming_tables AllButExternal;
   let unsafe_needs = {
-    mldummy = struct_ast_search ((==) MLdummy) struc;
-    tdummy = struct_type_search Mlutil.isDummy struc;
+    mldummy = struct_ast_search Mlutil.isMLdummy struc;
+    tdummy = struct_type_search Mlutil.isTdummy struc;
     tunknown = struct_type_search ((==) Tunknown) struc;
     magic =
       if lang () != Haskell then false
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 1112c3b89..f4d14af62 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -91,7 +91,7 @@ exception NotDefault of kill_reason
 let check_default env t =
   match flag_of_type env t with
     | _,TypeScheme -> raise (NotDefault Ktype)
-    | Logic,_ -> raise (NotDefault Kother)
+    | Logic,_ -> raise (NotDefault Kprop)
     | _ -> ()
 
 let is_info_scheme env t = match flag_of_type env t with
@@ -103,7 +103,7 @@ let is_info_scheme env t = match flag_of_type env t with
 let rec type_sign env c =
   match kind_of_term (whd_betadeltaiota env none c) with
     | Prod (n,t,d) ->
-	(if is_info_scheme env t then Keep else Kill Kother)
+	(if is_info_scheme env t then Keep else Kill Kprop)
 	:: (type_sign (push_rel_assum (n,t) env) d)
     | _ -> []
 
@@ -137,7 +137,7 @@ let rec type_sign_vl env c =
   match kind_of_term (whd_betadeltaiota env none c) with
     | Prod (n,t,d) ->
 	let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in
-	if not (is_info_scheme env t) then Kill Kother::s, vl
+	if not (is_info_scheme env t) then Kill Kprop::s, vl
 	else Keep::s, (make_typvar n vl) :: vl
     | _ -> [],[]
 
@@ -154,25 +154,12 @@ let sign_with_implicits r s nb_params =
   let implicits = implicits_of_global r in
   let rec add_impl i = function
     | [] -> []
-    | sign::s ->
-	let sign' =
-	  if sign == Keep && Int.List.mem i implicits
-          then Kill Kother else sign
-	in sign' :: add_impl (succ i) s
+    | Keep::s when Int.Set.mem i implicits ->
+       Kill (Kimplicit (r,i)) :: add_impl (i+1) s
+    | sign::s -> sign :: add_impl (i+1) s
   in
   add_impl (1+nb_params) s
 
-(* Enriching a exception message *)
-
-let rec handle_exn r n fn_name = function
-  | MLexn s ->
-      (try Scanf.sscanf s "UNBOUND %d%!"
-	 (fun i ->
-	    assert ((0 < i) && (i <= n));
-	    MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i)))
-       with Scanf.Scan_failure _ | End_of_file -> MLexn s)
-  | a -> ast_map (handle_exn r n fn_name) a
-
 (*S Management of type variable contexts. *)
 
 (* A De Bruijn variable context (db) is a context for translating Coq [Rel]
@@ -285,10 +272,10 @@ let rec extract_type env db j c args =
 	       (match expand env mld with
 		  | Tdummy d -> Tdummy d
 		  | _ ->
-		      let reason = if lvl == TypeScheme then Ktype else Kother in
+		      let reason = if lvl == TypeScheme then Ktype else Kprop in
 		      Tarr (Tdummy reason, mld)))
     | Sort _ -> Tdummy Ktype (* The two logical cases. *)
-    | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kother
+    | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kprop
     | Rel n ->
 	(match lookup_rel n env with
            | (_,Some t,_) -> extract_type env db j (lift n t) args
@@ -458,7 +445,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	if p.ip_logical then raise (I Standard);
 	if not (Int.equal (Array.length p.ip_types) 1) then raise (I Standard);
 	let typ = p.ip_types.(0) in
-	let l = List.filter (fun t -> not (isDummy (expand env t))) typ in
+	let l = List.filter (fun t -> not (isTdummy (expand env t))) typ in
 	if not (keep_singleton ()) &&
 	    Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l))
 	then raise (I Singleton);
@@ -479,7 +466,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	let mp = MutInd.modpath kn in
 	let rec select_fields l typs = match l,typs with
 	  | [],[] -> []
-	  | _::l, typ::typs when isDummy (expand env typ) ->
+	  | _::l, typ::typs when isTdummy (expand env typ) ->
 	      select_fields l typs
 	  | Anonymous::l, typ::typs ->
 	      None :: (select_fields l typs)
@@ -655,7 +642,7 @@ and extract_maybe_term env mle mlt c =
   try check_default env (type_of env c);
     extract_term env mle mlt c []
   with NotDefault d ->
-    put_magic (mlt, Tdummy d) MLdummy
+    put_magic (mlt, Tdummy d) (MLdummy d)
 
 (*s Generic way to deal with an application. *)
 
@@ -723,11 +710,11 @@ and extract_cst_app env mle mlt kn u args =
 	else mla
       with e when Errors.noncritical e -> mla
   in
-  (* For strict languages, purely logical signatures with at least
-     one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
+  (* For strict languages, purely logical signatures lead to a dummy lam
+     (except when [Kill Ktype] everywhere). So a [MLdummy] is left
      accordingly. *)
   let optdummy = match sign_kind s_full with
-    | UnsafeLogicalSig when lang () != Haskell -> [MLdummy]
+    | UnsafeLogicalSig when lang () != Haskell -> [MLdummy Kprop]
     | _ -> []
   in
   (* Different situations depending of the number of arguments: *)
@@ -826,8 +813,8 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	(* Logical singleton case: *)
 	(* [match c with C i j k -> t] becomes [t'] *)
 	assert (Int.equal br_size 1);
-	let s = iterate (fun l -> Kill Kother :: l) ni.(0) [] in
-	let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni.(0) mlt in
+	let s = iterate (fun l -> Kill Kprop :: l) ni.(0) [] in
+	let mlt = iterate (fun t -> Tarr (Tdummy Kprop, t)) ni.(0) mlt in
 	let e = extract_maybe_term env mle mlt br.(0) in
 	snd (case_expunge s e)
       end
@@ -851,8 +838,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in
 	(* We suppress dummy arguments according to signature. *)
 	let ids,e = case_expunge s e in
-	let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in
-	(List.rev ids, Pusual r, e')
+	(List.rev ids, Pusual r, e)
       in
       if mi.ind_kind == Singleton then
 	begin
@@ -960,8 +946,6 @@ let extract_std_constant env kn body typ =
   let e = extract_term env mle t' c [] in
   (* Expunging term and type from dummy lambdas. *)
   let trm = term_expunge s (ids,e) in
-  let trm = handle_exn (ConstRef kn) n (fun i -> fst (List.nth rels (i-1))) trm
-  in
   trm, type_expunge_from_sign env s t
 
 (* Extracts the type of an axiom, honors the Extraction Implicit declaration. *)
@@ -979,8 +963,8 @@ let extract_axiom env kn typ =
 
 let extract_fixpoint env vkn (fi,ti,ci) =
   let n = Array.length vkn in
-  let types = Array.make n (Tdummy Kother)
-  and terms = Array.make n MLdummy in
+  let types = Array.make n (Tdummy Kprop)
+  and terms = Array.make n (MLdummy Kprop) in
   let kns = Array.to_list vkn in
   current_fixpoints := kns;
   (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
@@ -1022,7 +1006,7 @@ let extract_constant env kn cb =
   in
   match flag_of_type env typ with
     | (Logic,TypeScheme) -> warn_log (); Dtype (r, [], Tdummy Ktype)
-    | (Logic,Default) -> warn_log (); Dterm (r, MLdummy, Tdummy Kother)
+    | (Logic,Default) -> warn_log (); Dterm (r, MLdummy Kprop, Tdummy Kprop)
     | (Info,TypeScheme) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_typ_ax ()
@@ -1047,7 +1031,7 @@ let extract_constant_spec env kn cb =
   let typ = Typeops.type_of_constant_type env cb.const_type in
   match flag_of_type env typ with
     | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
-    | (Logic, Default) -> Sval (r, Tdummy Kother)
+    | (Logic, Default) -> Sval (r, Tdummy Kprop)
     | (Info, TypeScheme) ->
 	let s,vl = type_sign_vl env typ in
 	(match cb.const_body with
@@ -1075,8 +1059,8 @@ let extract_constr env c =
   reset_meta_count ();
   let typ = type_of env c in
   match flag_of_type env typ with
-    | (_,TypeScheme) -> MLdummy, Tdummy Ktype
-    | (Logic,_) -> MLdummy, Tdummy Kother
+    | (_,TypeScheme) -> MLdummy Ktype, Tdummy Ktype
+    | (Logic,_) -> MLdummy Kprop, Tdummy Kprop
     | (Info,Default) ->
       let mlt = extract_type env [] 1 typ [] in
       extract_term env Mlenv.empty mlt c [], mlt
@@ -1090,7 +1074,7 @@ let extract_inductive env kn =
       | [] -> []
       | t::l ->
 	  let l' = filter (succ i) l in
-	  if isDummy (expand env t) || Int.List.mem i implicits then l'
+	  if isTdummy (expand env t) || Int.Set.mem i implicits then l'
 	  else t::l'
     in filter (1+ind.ind_nparams) l
   in
@@ -1102,11 +1086,11 @@ let extract_inductive env kn =
 (*s Is a [ml_decl] logical ? *)
 
 let logical_decl = function
-  | Dterm (_,MLdummy,Tdummy _) -> true
+  | Dterm (_,MLdummy _,Tdummy _) -> true
   | Dtype (_,[],Tdummy _) -> true
   | Dfix (_,av,tv) ->
-      (Array.for_all ((==) MLdummy) av) &&
-      (Array.for_all isDummy tv)
+      (Array.for_all isMLdummy av) &&
+      (Array.for_all isTdummy tv)
   | Dind (_,i) -> Array.for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 37b414207..530eb2ff8 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -200,8 +200,11 @@ let rec pp_expr par env args =
     | MLexn s ->
 	(* An [MLexn] may be applied, but I don't really care. *)
 	pp_par par (str "Prelude.error" ++ spc () ++ qs s)
-    | MLdummy ->
-	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
+    | MLdummy k ->
+        (* An [MLdummy] may be applied, but I don't really care. *)
+        (match msg_of_implicit k with
+         | "" -> str "__"
+         | s -> str "__" ++ spc () ++ pp_bracket_comment (str s))
     | MLmagic a ->
 	pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
     | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index 125dc86b8..df79c585e 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -153,7 +153,7 @@ let rec json_expr env = function
       ("what", json_str "expr:exception");
       ("msg", json_str s)
     ]
-  | MLdummy -> json_dict [("what", json_str "expr:dummy")]
+  | MLdummy _ -> json_dict [("what", json_str "expr:dummy")]
   | MLmagic a -> json_dict [
       ("what", json_str "expr:coerce");
       ("value", json_expr env a)
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index b7dee6cb1..681dceaa0 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -16,11 +16,16 @@ open Globnames
    object expects, and what these arguments will become in the ML
    object. *)
 
-(* We eliminate from terms:  1) types 2) logical parts.
-   [Kother] stands both for logical or other reasons
-   (for instance user-declared implicit arguments w.r.t. extraction). *)
+(* We eliminate from terms:
+   1) types
+   2) logical parts
+   3) user-declared implicit arguments of a constant of constructor
+*)
 
-type kill_reason = Ktype | Kother
+type kill_reason =
+  | Ktype
+  | Kprop
+  | Kimplicit of global_reference * int  (* n-th arg of a cst or construct *)
 
 type sign = Keep | Kill of kill_reason
 
@@ -118,7 +123,7 @@ and ml_ast =
   | MLcase   of ml_type * ml_ast * ml_branch array
   | MLfix    of int * Id.t array * ml_ast array
   | MLexn    of string
-  | MLdummy
+  | MLdummy  of kill_reason
   | MLaxiom
   | MLmagic  of ml_ast
 
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 6fc1195fb..402370eec 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -299,10 +299,12 @@ let type_to_signature env t =
 
 let isKill = function Kill _ -> true | _ -> false
 
-let isDummy = function Tdummy _ -> true | _ -> false
+let isTdummy = function Tdummy _ -> true | _ -> false
+
+let isMLdummy = function MLdummy _ -> true | _ -> false
 
 let sign_of_id = function
-  | Dummy -> Kill Kother
+  | Dummy -> Kill Kprop
   | _ -> Keep
 
 (* Classification of signatures *)
@@ -310,45 +312,44 @@ let sign_of_id = function
 type sign_kind =
   | EmptySig
   | NonLogicalSig (* at least a [Keep] *)
-  | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *)
   | SafeLogicalSig (* only [Kill Ktype] *)
+  | UnsafeLogicalSig (* No [Keep], not all [Kill Ktype] *)
 
 let rec sign_kind = function
   | [] -> EmptySig
   | Keep :: _ -> NonLogicalSig
   | Kill k :: s ->
-      match sign_kind s with
-	| NonLogicalSig -> NonLogicalSig
-	| UnsafeLogicalSig -> UnsafeLogicalSig
-	| SafeLogicalSig | EmptySig ->
-	    if k == Kother then UnsafeLogicalSig else SafeLogicalSig
+     match k, sign_kind s with
+     | _, NonLogicalSig -> NonLogicalSig
+     | Ktype, (SafeLogicalSig | EmptySig) -> SafeLogicalSig
+     | _, _ -> UnsafeLogicalSig
 
 (* Removing the final [Keep] in a signature *)
 
 let rec sign_no_final_keeps = function
   | [] -> []
   | k :: s ->
-      let s' = k :: sign_no_final_keeps s in
-      match s' with [Keep] -> [] | _ -> s'
+     match k, sign_no_final_keeps s with
+     | Keep, [] -> []
+     | k, l -> k::l
 
 (*s Removing [Tdummy] from the top level of a ML type. *)
 
 let type_expunge_from_sign env s t =
-  let rec expunge s t =
-    if List.is_empty s then t else match t with
-      | Tmeta {contents = Some t} -> expunge s t
-      | Tarr (a,b) ->
-	  let t = expunge (List.tl s) b in
-	  if List.hd s == Keep then Tarr (a, t) else t
-      | Tglob (r,l) ->
-	  (match env r with
-	     | Some mlt -> expunge s (type_subst_list l mlt)
-	     | None -> assert false)
-      | _ -> assert false
+  let rec expunge s t = match s, t with
+    | [], _ -> t
+    | Keep :: s, Tarr(a,b) -> Tarr (a, expunge s b)
+    | Kill _ :: s, Tarr(a,b) -> expunge s b
+    | _, Tmeta {contents = Some t} -> expunge s t
+    | _, Tglob (r,l) ->
+       (match env r with
+	| Some mlt -> expunge s (type_subst_list l mlt)
+	| None -> assert false)
+    | _ -> assert false
   in
   let t = expunge (sign_no_final_keeps s) t in
   if lang () != Haskell && sign_kind s == UnsafeLogicalSig then
-    Tarr (Tdummy Kother, t)
+    Tarr (Tdummy Kprop, t)
   else t
 
 let type_expunge env t =
@@ -385,7 +386,7 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with
 | MLfix (i1, id1, t1), MLfix (i2, id2, t2) ->
   Int.equal i1 i2 && Array.equal Id.equal id1 id2 && Array.equal eq_ml_ast t1 t2
 | MLexn e1, MLexn e2 -> String.equal e1 e2
-| MLdummy, MLdummy -> true
+| MLdummy k1, MLdummy k2 -> k1 == k2
 | MLaxiom, MLaxiom -> true
 | MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2
 | _ -> false
@@ -420,7 +421,7 @@ let ast_iter_rel f =
     | MLapp (a,l) -> iter n a; List.iter (iter n) l
     | MLcons (_,_,l) | MLtuple l ->  List.iter (iter n) l
     | MLmagic a -> iter n a
-    | MLglob _ | MLexn _ | MLdummy | MLaxiom -> ()
+    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> ()
   in iter 0
 
 (*s Map over asts. *)
@@ -439,7 +440,7 @@ let ast_map f = function
   | MLcons (typ,c,l) -> MLcons (typ,c, List.map f l)
   | MLtuple l -> MLtuple (List.map f l)
   | MLmagic a -> MLmagic (f a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom as a -> a
 
 (*s Map over asts, with binding depth as parameter. *)
 
@@ -457,7 +458,7 @@ let ast_map_lift f n = function
   | MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l)
   | MLtuple l -> MLtuple (List.map (f n) l)
   | MLmagic a -> MLmagic (f n a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom as a -> a
 
 (*s Iter over asts. *)
 
@@ -471,7 +472,7 @@ let ast_iter f = function
   | MLapp (a,l) -> f a; List.iter f l
   | MLcons (_,_,l) | MLtuple l -> List.iter f l
   | MLmagic a -> f a
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom  -> ()
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom  -> ()
 
 (*S Operations concerning De Bruijn indices. *)
 
@@ -507,7 +508,7 @@ let nb_occur_match =
     | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
     | MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l
     | MLmagic a -> nb k a
-    | MLglob _ | MLexn _ | MLdummy | MLaxiom -> 0
+    | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> 0
   in nb 1
 
 (*s Lifting on terms.
@@ -559,7 +560,7 @@ let gen_subst v d t =
 	if i' < 1 then a
 	else if i' <= Array.length v then
 	  match v.(i'-1) with
-	    | None -> MLexn ("UNBOUND " ^ string_of_int i')
+	    | None -> assert false
 	    | Some u -> ast_lift n u
 	else MLrel (i+d)
     | a -> ast_map_lift subst n a
@@ -813,8 +814,8 @@ let census_add, census_max, census_clean =
     try h := add k i !h
     with Not_found -> h := (k, Int.Set.singleton i) :: !h
   in
-  let maxf k =
-    let len = ref 0 and lst = ref Int.Set.empty and elm = ref k in
+  let maxf () =
+    let len = ref 0 and lst = ref Int.Set.empty and elm = ref MLaxiom in
     List.iter
       (fun (e, s) ->
 	 let n = Int.Set.cardinal s in
@@ -843,7 +844,7 @@ let factor_branches o typ br =
       if o.opt_case_cst then
 	(try census_add (branch_as_cst br.(i)) i with Impossible -> ());
     done;
-    let br_factor, br_set = census_max MLdummy in
+    let br_factor, br_set = census_max () in
     census_clean ();
     let n = Int.Set.cardinal br_set in
     if Int.equal n 0 then None
@@ -926,7 +927,7 @@ let iota_gen br hd =
   in iota 0 hd
 
 let is_atomic = function
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy _ -> true
   | _ -> false
 
 let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false
@@ -998,7 +999,7 @@ and simpl_app o a = function
 	     let a' = List.map (ast_lift k) a in
 	     (l, p, simpl o (MLapp (t,a')))) br
       in simpl o (MLcase (typ,e,br'))
-  | (MLdummy | MLexn _) as e -> e
+  | (MLdummy _ | MLexn _) as e -> e
 	(* We just discard arguments in those cases. *)
   | f -> MLapp (f,a)
 
@@ -1049,20 +1050,26 @@ let rec select_via_bl l args = match l,args with
 (*s [kill_some_lams] removes some head lambdas according to the signature [bl].
    This list is build on the identifier list model: outermost lambda
    is on the right.
-   [Rels] corresponding to removed lambdas are supposed not to occur, and
+   [Rels] corresponding to removed lambdas are not supposed to occur
+   (except maybe in the case of Kimplicit), and
    the other [Rels] are made correct via a [gen_subst].
    Output is not directly a [ml_ast], compose with [named_lams] if needed. *)
 
+let is_impl_kill = function Kill (Kimplicit _) -> true | _ -> false
+
 let kill_some_lams bl (ids,c) =
   let n = List.length bl in
   let n' = List.fold_left (fun n b -> if b == Keep then (n+1) else n) 0 bl in
   if Int.equal n n' then ids,c
-  else if Int.equal n' 0 then [],ast_lift (-n) c
+  else if Int.equal n' 0 && not (List.exists is_impl_kill bl)
+  then [],ast_lift (-n) c
   else begin
     let v = Array.make n None in
     let rec parse_ids i j = function
       | [] -> ()
       | Keep :: l -> v.(i) <- Some (MLrel j); parse_ids (i+1) (j+1) l
+      | Kill (Kimplicit _ as k) :: l ->
+         v.(i) <- Some (MLdummy k); parse_ids (i+1) j l
       | Kill _ :: l -> parse_ids (i+1) j l
     in parse_ids 0 1 bl;
     select_via_bl bl ids, gen_subst v (n'-n) c
@@ -1100,12 +1107,12 @@ let eta_expansion_sign s (ids,c) =
 	let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels
 	in ids, MLapp (ast_lift (i-1) c, a)
     | Keep :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l
-    | Kill _ :: l -> abs (Dummy :: ids) (MLdummy :: rels) (i+1) l
+    | Kill k :: l -> abs (Dummy :: ids) (MLdummy k :: rels) (i+1) l
   in abs ids [] 1 s
 
 (*s If [s = [b1; ... ; bn]] then [case_expunge] decomposes [e]
   in [n] lambdas (with eta-expansion if needed) and removes all dummy lambdas
-  corresponding to [Del] in [s]. *)
+  corresponding to [Kill _] in [s]. *)
 
 let case_expunge s e =
   let m = List.length s in
@@ -1123,8 +1130,9 @@ let term_expunge s (ids,c) =
   if List.is_empty s then c
   else
     let ids,c = kill_some_lams (List.rev s) (ids,c) in
-    if List.is_empty ids && lang () != Haskell && List.mem (Kill Kother) s then
-      MLlam (Dummy, ast_lift 1 c)
+    if List.is_empty ids && lang () != Haskell &&
+       sign_kind s == UnsafeLogicalSig
+    then MLlam (Dummy, ast_lift 1 c)
     else named_lams ids c
 
 (*s [kill_dummy_args ids r t] looks for occurrences of [MLrel r] in [t] and
@@ -1267,7 +1275,7 @@ let rec ml_size = function
   | MLfix(_,_,f) -> ml_size_array f
   | MLletin (_,_,t) -> ml_size t
   | MLmagic t -> ml_size t
-  | MLglob _ | MLrel _ | MLexn _ | MLdummy | MLaxiom -> 0
+  | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom -> 0
 
 and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l
 
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 0a71d2c83..c380dfb3e 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -67,7 +67,8 @@ val type_expunge : abbrev_map -> ml_type -> ml_type
 val type_expunge_from_sign : abbrev_map -> signature -> ml_type -> ml_type
 
 val eq_ml_type : ml_type -> ml_type -> bool
-val isDummy : ml_type -> bool
+val isTdummy : ml_type -> bool
+val isMLdummy : ml_ast -> bool
 val isKill : sign -> bool
 
 val case_expunge : signature -> ml_ast -> ml_ident list * ml_ast
@@ -125,8 +126,8 @@ exception Impossible
 type sign_kind =
   | EmptySig
   | NonLogicalSig (* at least a [Keep] *)
-  | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *)
   | SafeLogicalSig (* only [Kill Ktype] *)
+  | UnsafeLogicalSig (* No [Keep], not all [Kill Ktype] *)
 
 val sign_kind : signature -> sign_kind
 
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 53c9f5987..e8383bda5 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -100,7 +100,7 @@ let ast_iter_references do_term do_cons do_type a =
 	Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v
 
       | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _
-      | MLdummy | MLaxiom | MLmagic _ -> ()
+      | MLdummy _ | MLaxiom | MLmagic _ -> ()
   in iter a
 
 let ind_iter_references do_term do_cons do_type kn ind =
@@ -387,16 +387,15 @@ let is_prefix pre s =
   in
   is_prefix_aux 0
 
-let check_implicits = function
-  | MLexn s ->
-      if String.length s > 8 && (s.[0] == 'U' || s.[0] == 'I') then
-	begin
-	  if is_prefix "UNBOUND" s then assert false;
-	  if is_prefix "IMPLICIT" s then
-	    error_non_implicit (String.sub s 9 (String.length s - 9));
-	end;
-      false
-  | _ -> false
+exception RemainingImplicit of kill_reason
+
+let check_for_remaining_implicits struc =
+  let check = function
+    | MLdummy (Kimplicit _ as k) -> raise (RemainingImplicit k)
+    | _ -> false
+  in
+  try ignore (struct_ast_search check struc)
+  with RemainingImplicit k -> err_or_warn_remaining_implicit k
 
 let optimize_struct to_appear struc =
   let subst = ref (Refmap'.empty : ml_ast Refmap'.t) in
@@ -415,5 +414,5 @@ let optimize_struct to_appear struc =
         depcheck_struct opt_struc
       end
   in
-  ignore (struct_ast_search check_implicits mini_struc);
+  let () = check_for_remaining_implicits mini_struc in
   mini_struc
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 45f5614af..257c6e971 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -199,8 +199,11 @@ let rec pp_expr par env args =
     | MLexn s ->
 	(* An [MLexn] may be applied, but I don't really care. *)
 	pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)"))
-    | MLdummy ->
-	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
+    | MLdummy k ->
+        (* An [MLdummy] may be applied, but I don't really care. *)
+        (match msg_of_implicit k with
+         | "" -> str "__"
+         | s -> str "__" ++ spc () ++ str ("(* "^s^" *)"))
     | MLmagic a ->
 	pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args)
     | MLaxiom ->
@@ -352,7 +355,7 @@ and pp_function env t =
     | MLcase(Tglob(r,_),MLrel 1,pv) when
 	not (is_coinductive r) && List.is_empty (get_record_fields r) &&
 	not (is_custom_match pv) ->
-	if not (ast_occurs 1 (MLcase(Tunknown,MLdummy,pv))) then
+	if not (ast_occurs 1 (MLcase(Tunknown,MLaxiom,pv))) then
 	  pr_binding (List.rev (List.tl bl)) ++
        	  str " = function" ++ fnl () ++
 	  v 0 (pp_pat env' pv)
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index cc8b6d8e7..4901cf180 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -126,7 +126,7 @@ let rec pp_expr env args =
     | MLexn s ->
 	(* An [MLexn] may be applied, but I don't really care. *)
 	paren (str "error" ++ spc () ++ qs s)
-    | MLdummy ->
+    | MLdummy _ ->
 	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLmagic a ->
 	pp_expr env args a
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index a57c39eef..63d792e36 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -401,16 +401,34 @@ let error_MPfile_as_mod mp b =
 	    "Monolithic Extraction cannot deal with this situation.\n"^
 	    "Please "^s2^"use (Recursive) Extraction Library instead.\n"))
 
-let msg_non_implicit r n id =
-  let name = match id with
-    | Anonymous -> ""
-    | Name id -> "(" ^ Id.to_string id ^ ") "
-  in
-  "The " ^ (String.ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r)
-
-let error_non_implicit msg =
-  err (str (msg ^ " still occurs after extraction.") ++
-       fnl () ++ str "Please check the Extraction Implicit declarations.")
+let argnames_of_global r =
+  let typ = Global.type_of_global_unsafe r in
+  let rels,_ =
+    decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in
+  List.rev_map fst rels
+
+let msg_of_implicit = function
+  | Kimplicit (r,i) ->
+     let name = match List.nth (argnames_of_global r) (i-1) with
+       | Anonymous -> ""
+       | Name id -> "(" ^ Id.to_string id ^ ") "
+     in
+     (String.ordinal i)^" argument "^name^"of "^(string_of_global r)
+  | Ktype | Kprop -> ""
+
+let error_remaining_implicit k =
+  let s = msg_of_implicit k in
+  err (str ("An implicit occurs after extraction : "^s^".") ++ fnl () ++
+       str "Please check your Extraction Implicit declarations." ++ fnl() ++
+       str "You might also try Unset Extraction SafeImplicits to force" ++
+       fnl() ++ str "the extraction of unsafe code and review it manually.")
+
+let warning_remaining_implicit k =
+  let s = msg_of_implicit k in
+  msg_warning
+    (str ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++
+     str "Extraction SafeImplicits is unset, extracting nonetheless," ++ fnl ()
+     ++ str "but this code is potentially unsafe, please review it manually.")
 
 let check_loaded_modfile mp = match base_mp mp with
   | MPfile dp ->
@@ -635,32 +653,39 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
 (*s Extraction Implicit *)
 
+let safe_implicit = my_bool_option "SafeImplicits" true
+
+let err_or_warn_remaining_implicit k =
+  if safe_implicit () then
+    error_remaining_implicit k
+  else
+    warning_remaining_implicit k
+
 type int_or_id = ArgInt of int | ArgId of Id.t
 
 let implicits_table = Summary.ref Refmap'.empty ~name:"ExtrImplicit"
 
 let implicits_of_global r =
- try Refmap'.find r !implicits_table with Not_found -> []
+ try Refmap'.find r !implicits_table with Not_found -> Int.Set.empty
 
 let add_implicits r l =
-  let typ = Global.type_of_global_unsafe r in
-  let rels,_ =
-    decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in
-  let names = List.rev_map fst rels in
+  let names = argnames_of_global r in
   let n = List.length names in
-  let check = function
+  let add_arg s = function
     | ArgInt i ->
-	if 1 <= i && i <= n then i
+	if 1 <= i && i <= n then Int.Set.add i s
 	else err (int i ++ str " is not a valid argument number for " ++
 		  safe_pr_global r)
     | ArgId id ->
-	(try List.index Name.equal (Name id) names
-	 with Not_found ->
-	   err (str "No argument " ++ pr_id id ++ str " for " ++
-		safe_pr_global r))
+       try
+         let i = List.index Name.equal (Name id) names in
+         Int.Set.add i s
+       with Not_found ->
+	 err (str "No argument " ++ pr_id id ++ str " for " ++
+	      safe_pr_global r)
   in
-  let l' = List.map check l in
-  implicits_table := Refmap'.add r l' !implicits_table
+  let ints = List.fold_left add_arg Int.Set.empty l in
+  implicits_table := Refmap'.add r ints !implicits_table
 
 (* Registration of operations for rollback. *)
 
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. *)