Imported Upstream version 8.6upstream/8.6

13 files changed, 209 insertions, 171 deletions

diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v
index 9a1a4aa0..c9e8eac0 100644
--- a/plugins/extraction/ExtrOcamlZBigInt.v
+++ b/plugins/extraction/ExtrOcamlZBigInt.v
@@ -46,7 +46,7 @@ Extract Constant Pos.max => "Big.max".
 Extract Constant Pos.compare =>
  "fun x y -> Big.compare_case Eq Lt Gt x y".
 Extract Constant Pos.compare_cont =>
- "fun x y c -> Big.compare_case c Lt Gt x y".
+ "fun c x y -> Big.compare_case c Lt Gt x y".
 
 Extract Constant N.add => "Big.add".
 Extract Constant N.succ => "Big.succ".
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index bb9e8e5f..3c5f6cb7 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -17,8 +17,8 @@ open Table
 open Miniml
 open Mlutil
 
-let string_of_id id =
-  let s = Names.Id.to_string id in
+let ascii_of_id id =
+  let s = Id.to_string id in
   for i = 0 to String.length s - 2 do
     if s.[i] == '_' && s.[i+1] == '_' then warning_id s
   done;
@@ -73,18 +73,19 @@ let fnl2 () = fnl () ++ fnl ()
 
 let space_if = function true -> str " " | false -> mt ()
 
-let is_digit = function
-  | '0'..'9' -> true
-  | _ -> false
+let begins_with s prefix =
+  let len = String.length prefix in
+  String.length s >= len && String.equal (String.sub s 0 len) prefix
 
 let begins_with_CoqXX s =
   let n = String.length s in
   n >= 4 && s.[0] == 'C' && s.[1] == 'o' && s.[2] == 'q' &&
   let i = ref 3 in
   try while !i < n do
-    if s.[!i] == '_' then i:=n (*Stop*)
-    else if is_digit s.[!i] then incr i
-    else raise Not_found
+    match s.[!i] with
+    | '_' -> i:=n (*Stop*)
+    | '0'..'9' -> incr i
+    | _ -> raise Not_found
   done; true
   with Not_found -> false
 
@@ -109,9 +110,9 @@ let pseudo_qualify = qualify "__"
 let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
 let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
 
-let lowercase_id id = Id.of_string (String.uncapitalize (string_of_id id))
+let lowercase_id id = Id.of_string (String.uncapitalize (ascii_of_id id))
 let uppercase_id id =
-  let s = string_of_id id in
+  let s = ascii_of_id id in
   assert (not (String.is_empty s));
   if s.[0] == '_' then Id.of_string ("Coq_"^s)
   else Id.of_string (String.capitalize s)
@@ -331,13 +332,10 @@ let reset_renaming_tables flag =
    existing. *)
 
 let modular_rename k id =
-  let s = string_of_id id in
-  let prefix,is_ok =
-    if upperkind k then "Coq_",is_upper else "coq_",is_lower
+  let s = ascii_of_id id in
+  let prefix,is_ok = if upperkind k then "Coq_",is_upper else "coq_",is_lower
   in
-  if not (is_ok s) ||
-    (Id.Set.mem id (get_keywords ())) ||
-    (String.length s >= 4 && String.equal (String.sub s 0 4) prefix)
+  if not (is_ok s) || Id.Set.mem id (get_keywords ()) || begins_with s prefix
   then prefix ^ s
   else s
 
@@ -345,21 +343,20 @@ let modular_rename k id =
     with unique numbers *)
 
 let modfstlev_rename =
-  let add_prefixes,get_prefixes,_ = mktable_id true in
+  let add_index,get_index,_ = mktable_id true in
   fun l ->
-    let coqid = Id.of_string "Coq" in
     let id = Label.to_id l in
     try
-      let coqset = get_prefixes id in
-      let nextcoq = next_ident_away coqid coqset in
-      add_prefixes id (nextcoq::coqset);
-      (string_of_id nextcoq)^"_"^(string_of_id id)
+      let n = get_index id in
+      add_index id (n+1);
+      let s = if n == 0 then "" else string_of_int (n-1) in
+      "Coq"^s^"_"^(ascii_of_id id)
     with Not_found ->
-      let s = string_of_id id in
+      let s = ascii_of_id id in
       if is_lower s || begins_with_CoqXX s then
-	(add_prefixes id [coqid]; "Coq_"^s)
+	(add_index id 1; "Coq_"^s)
       else
-	(add_prefixes id []; s)
+	(add_index id 0; s)
 
 (*s Creating renaming for a [module_path] : first, the real function ... *)
 
@@ -404,7 +401,7 @@ let ref_renaming_fun (k,r) =
     | [""] -> (* this happens only at toplevel of the monolithic case *)
       let globs = Id.Set.elements (get_global_ids ()) in
       let id = next_ident_away (kindcase_id k idg) globs in
-      string_of_id id
+      Id.to_string id
     | _ -> modular_rename k idg
   in
   add_global_ids (Id.of_string s);
@@ -562,7 +559,7 @@ let pp_ocaml_extern k base rls = match rls with
 	(* Standard situation : object in an opened file *)
 	dottify rls'
 
-(* [pp_ocaml_gen] : choosing between [pp_ocaml_extern] or [pp_ocaml_extern] *)
+(* [pp_ocaml_gen] : choosing between [pp_ocaml_local] or [pp_ocaml_extern] *)
 
 let pp_ocaml_gen k mp rls olab =
   match common_prefix_from_list mp (get_visible_mps ()) with
@@ -579,8 +576,7 @@ let pp_haskell_gen k mp rls = match rls with
   | s::rls' ->
     let str = pseudo_qualify rls' in
     let str = if is_upper str && not (upperkind k) then ("_"^str) else str in
-    let prf = if not (ModPath.equal (base_mp mp) (top_visible_mp ())) then s ^ "." else "" in
-    prf ^ str
+    if ModPath.equal (base_mp mp) (top_visible_mp ()) then str else s^"."^str
 
 (* Main name printing function for a reference *)
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 41a068ff..52f22ee6 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -13,13 +13,12 @@ open Names
 open Libnames
 open Globnames
 open Pp
-open Errors
+open CErrors
 open Util
 open Table
 open Extraction
 open Modutil
 open Common
-open Mod_subst
 
 (***************************************)
 (*S Part I: computing Coq environment. *)
@@ -542,7 +541,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
     (if dry then None else si);
   (* Print the buffer content via Coq standard formatter (ok with coqide). *)
   if not (Int.equal (Buffer.length buf) 0) then begin
-    Pp.msg_notice (str (Buffer.contents buf));
+    Feedback.msg_notice (str (Buffer.contents buf));
     Buffer.reset buf
   end
 
@@ -584,8 +583,8 @@ let rec locate_ref = function
 	| None, Some r -> let refs,mps = locate_ref l in r::refs,mps
 	| Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps
 	| Some mp, Some r ->
-	    warning_both_mod_and_cst q mp r;
-	    let refs,mps = locate_ref l in refs,mp::mps
+           warning_ambiguous_name (q,mp,r);
+           let refs,mps = locate_ref l in refs,mp::mps
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
     \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when
@@ -636,7 +635,7 @@ let simple_extraction r =
       in
       let ans = flag ++ print_one_decl struc (modpath_of_r r) d in
       reset ();
-      Pp.msg_notice ans
+      Feedback.msg_notice ans
   | _ -> assert false
 
 
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 10644da2..a980a43f 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -11,7 +11,6 @@ open Util
 open Names
 open Term
 open Vars
-open Context
 open Declarations
 open Declareops
 open Environ
@@ -26,6 +25,7 @@ open Globnames
 open Miniml
 open Table
 open Mlutil
+open Context.Rel.Declaration
 (*i*)
 
 exception I of inductive_kind
@@ -35,17 +35,18 @@ let current_fixpoints = ref ([] : constant list)
 
 let none = Evd.empty
 
+(* NB: In OCaml, [type_of] and [get_of] might raise
+   [SingletonInductiveBecomeProp]. This exception will be caught
+   in late wrappers around the exported functions of this file,
+   in order to display the location of the issue. *)
+
 let type_of env c =
-  try
-    let polyprop = (lang() == Haskell) in
-    Retyping.get_type_of ~polyprop env none (strip_outer_cast c)
-  with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
+  let polyprop = (lang() == Haskell) in
+  Retyping.get_type_of ~polyprop env none (strip_outer_cast c)
 
 let sort_of env c =
-  try
-    let polyprop = (lang() == Haskell) in
-    Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c)
-  with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
+  let polyprop = (lang() == Haskell) in
+  Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c)
 
 (*S Generation of flags and signatures. *)
 
@@ -73,9 +74,9 @@ type flag = info * scheme
   Really important function. *)
 
 let rec flag_of_type env t : flag =
-  let t = whd_betadeltaiota env none t in
+  let t = whd_all env none t in
   match kind_of_term t with
-    | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c
+    | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c
     | Sort s when Sorts.is_prop s -> (Logic,TypeScheme)
     | Sort _ -> (Info,TypeScheme)
     | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default)
@@ -101,14 +102,14 @@ let is_info_scheme env t = match flag_of_type env t with
 (*s [type_sign] gernerates a signature aimed at treating a type application. *)
 
 let rec type_sign env c =
-  match kind_of_term (whd_betadeltaiota env none c) with
+  match kind_of_term (whd_all env none c) with
     | Prod (n,t,d) ->
 	(if is_info_scheme env t then Keep else Kill Kprop)
 	:: (type_sign (push_rel_assum (n,t) env) d)
     | _ -> []
 
 let rec type_scheme_nb_args env c =
-  match kind_of_term (whd_betadeltaiota env none c) with
+  match kind_of_term (whd_all env none c) with
     | Prod (n,t,d) ->
 	let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in
 	if is_info_scheme env t then n+1 else n
@@ -134,7 +135,7 @@ let make_typvar n vl =
   next_ident_away id' vl
 
 let rec type_sign_vl env c =
-  match kind_of_term (whd_betadeltaiota env none c) with
+  match kind_of_term (whd_all 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 Kprop::s, vl
@@ -142,7 +143,7 @@ let rec type_sign_vl env c =
     | _ -> [],[]
 
 let rec nb_default_params env c =
-  match kind_of_term (whd_betadeltaiota env none c) with
+  match kind_of_term (whd_all env none c) with
     | Prod (n,t,d) ->
 	let n = nb_default_params (push_rel_assum (n,t) env) d in
 	if is_default env t then n+1 else n
@@ -248,7 +249,7 @@ let rec extract_type env db j c args =
     | _ 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
+           | LocalDef (_,t,_) -> extract_type env db j (lift n t) args
 	   | _ ->
 	       (* Asks [db] a translation for [n]. *)
 	       if n > List.length db then Tunknown
@@ -285,7 +286,7 @@ let rec extract_type env db j c args =
     | Ind ((kn,i),u) ->
 	let s = (extract_ind env kn).ind_packets.(i).ip_sign in
 	extract_type_app env db (IndRef (kn,i),s) args
-    | Case _ | Fix _ | CoFix _ -> Tunknown
+    | Case _ | Fix _ | CoFix _ | Proj _ -> Tunknown
     | _ -> assert false
 
 (*s Auxiliary function dealing with type application.
@@ -328,11 +329,22 @@ and extract_type_scheme env db c p =
 
 (*S Extraction of an inductive type. *)
 
+(* First, a version with cache *)
+
 and extract_ind env kn = (* kn is supposed to be in long form *)
   let mib = Environ.lookup_mind kn env in
   match lookup_ind kn mib with
   | Some ml_ind -> ml_ind
   | None ->
+     try
+       extract_really_ind env kn mib
+     with SingletonInductiveBecomesProp id ->
+       (* TODO : which inductive is concerned in the block ? *)
+       error_singleton_become_prop id (Some (IndRef (kn,0)))
+
+(* Then the real function *)
+
+and extract_really_ind env kn mib =
     (* First, if this inductive is aliased via a Module,
        we process the original inductive if possible.
        When at toplevel of the monolithic case, we cannot do much
@@ -359,8 +371,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     let packets =
       Array.mapi
 	(fun i mip ->
-	   let (ind,u), ctx = 
-	     Universes.fresh_inductive_instance env (kn,i) in
+	   let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in
 	   let ar = Inductive.type_of_inductive env ((mib,mip),u) in
 	   let info = (fst (flag_of_type env ar) = Info) in
 	   let s,v = if info then type_sign_vl env ar else [],[] in
@@ -477,7 +488,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 *)
 
 and extract_type_cons env db dbmap c i =
-  match kind_of_term (whd_betadeltaiota env none c) with
+  match kind_of_term (whd_all env none c) with
     | Prod (n,t,d) ->
 	let env' = push_rel_assum (n,t) env in
 	let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in
@@ -561,7 +572,7 @@ let rec extract_term env mle mlt c args =
 	       put_magic_if magic (MLlam (id, d')))
     | LetIn (n, c1, t1, c2) ->
 	let id = id_of_name n in
-	let env' = push_rel (Name id, Some c1, t1) env in
+	let env' = push_rel (LocalDef (Name id, c1, t1)) env in
 	(* We directly push the args inside the [LetIn].
            TODO: the opt_let_app flag is supposed to prevent that *)
 	let args' = List.map (lift 1) args in
@@ -579,10 +590,10 @@ let rec extract_term env mle mlt c args =
 	with NotDefault d ->
 	  let mle' = Mlenv.push_std_type mle (Tdummy d) in
 	  ast_pop (extract_term env' mle' mlt c2 args'))
-    | Const (kn,u) ->
-	extract_cst_app env mle mlt kn u args
-    | Construct (cp,u) ->
-	extract_cons_app env mle mlt cp u args
+    | Const (kn,_) ->
+	extract_cst_app env mle mlt kn args
+    | Construct (cp,_) ->
+	extract_cons_app env mle mlt cp args
     | Proj (p, c) ->
         let term = Retyping.expand_projection env (Evd.from_env env) p c [] in
 	  extract_term env mle mlt term args
@@ -633,7 +644,7 @@ and make_mlargs env e s args typs =
 
 (*s Extraction of a constant applied to arguments. *)
 
-and extract_cst_app env mle mlt kn u args =
+and extract_cst_app env mle mlt kn args =
   (* First, the [ml_schema] of the constant, in expanded version. *)
   let nb,t = record_constant_type env kn None in
   let schema = nb, expand env t in
@@ -672,7 +683,7 @@ and extract_cst_app env mle mlt kn u args =
 	let l,l' = List.chop (projection_arity (ConstRef kn)) mla in
 	if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
 	else mla
-      with e when Errors.noncritical e -> mla
+      with e when CErrors.noncritical e -> mla
   in
   (* For strict languages, purely logical signatures lead to a dummy lam
      (except when [Kill Ktype] everywhere). So a [MLdummy] is left
@@ -706,7 +717,7 @@ and extract_cst_app env mle mlt kn u args =
    they are fixed, and thus are not used for the computation.
    \end{itemize} *)
 
-and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args =
+and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   (* First, we build the type of the constructor, stored in small pieces. *)
   let mi = extract_ind env kn in
   let params_nb = mi.ind_nparams in
@@ -836,7 +847,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
 
 let decomp_lams_eta_n n m env c t =
   let rels = fst (splay_prod_n env none n t) in
-  let rels = List.map (fun (id,_,c) -> (id,c)) rels in
+  let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,c)) rels in
   let rels',c = decompose_lam c in
   let d = n - m in
   (* we'd better keep rels' as long as possible. *)
@@ -934,11 +945,13 @@ let extract_fixpoint env vkn (fi,ti,ci) =
   (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
   let sub = List.rev_map mkConst kns in
   for i = 0 to n-1 do
-    if sort_of env ti.(i) != InProp then begin
-      let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in
-      terms.(i) <- e;
-      types.(i) <- t;
-    end
+    if sort_of env ti.(i) != InProp then
+      try
+        let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in
+        terms.(i) <- e;
+        types.(i) <- t;
+      with SingletonInductiveBecomesProp id ->
+        error_singleton_become_prop id (Some (ConstRef vkn.(i)))
   done;
   current_fixpoints := [];
   Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types)
@@ -968,13 +981,17 @@ let extract_constant env kn cb =
     let e,t = extract_std_constant env kn c typ in
     Dterm (r,e,t)
   in
-  match flag_of_type env typ with
+  try
+    match flag_of_type env typ with
     | (Logic,TypeScheme) -> warn_log (); Dtype (r, [], Tdummy Ktype)
     | (Logic,Default) -> warn_log (); Dterm (r, MLdummy Kprop, Tdummy Kprop)
     | (Info,TypeScheme) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_typ_ax ()
-	  | Def c -> mk_typ (Mod_subst.force_constr c)
+	  | Def c ->
+	     (match cb.const_proj with
+	      | None -> mk_typ (Mod_subst.force_constr c)
+	      | Some pb -> mk_typ pb.proj_body)
 	  | OpaqueDef c ->
 	    add_opaque r;
 	    if access_opaque () then
@@ -983,17 +1000,23 @@ let extract_constant env kn cb =
     | (Info,Default) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_ax ()
-	  | Def c -> mk_def (Mod_subst.force_constr c)
+	  | Def c ->
+	     (match cb.const_proj with
+	      | None -> mk_def (Mod_subst.force_constr c)
+	      | Some pb -> mk_def pb.proj_body)
 	  | OpaqueDef c ->
 	    add_opaque r;
 	    if access_opaque () then
               mk_def (Opaqueproof.force_proof (Environ.opaque_tables env) c)
             else mk_ax ())
+  with SingletonInductiveBecomesProp id ->
+    error_singleton_become_prop id (Some (ConstRef kn))
 
 let extract_constant_spec env kn cb =
   let r = ConstRef kn in
   let typ = Typeops.type_of_constant_type env cb.const_type in
-  match flag_of_type env typ with
+  try
+    match flag_of_type env typ with
     | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
     | (Logic, Default) -> Sval (r, Tdummy Kprop)
     | (Info, TypeScheme) ->
@@ -1008,26 +1031,34 @@ let extract_constant_spec env kn cb =
     | (Info, Default) ->
 	let t = snd (record_constant_type env kn (Some typ)) in
 	Sval (r, type_expunge env t)
+  with SingletonInductiveBecomesProp id ->
+    error_singleton_become_prop id (Some (ConstRef kn))
 
 let extract_with_type env c =
-  let typ = type_of env c in
-  match flag_of_type env typ with
+  try
+    let typ = type_of env c in
+    match flag_of_type env typ with
     | (Info, TypeScheme) ->
 	let s,vl = type_sign_vl env typ in
 	let db = db_from_sign s in
 	let t = extract_type_scheme env db c (List.length s) in
 	Some (vl, t)
     | _ -> None
+  with SingletonInductiveBecomesProp id ->
+    error_singleton_become_prop id None
 
 let extract_constr env c =
   reset_meta_count ();
-  let typ = type_of env c in
-  match flag_of_type env typ with
+  try
+    let typ = type_of env c in
+    match flag_of_type env typ with
     | (_,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
+       let mlt = extract_type env [] 1 typ [] in
+       extract_term env Mlenv.empty mlt c [], mlt
+  with SingletonInductiveBecomesProp id ->
+    error_singleton_become_prop id None
 
 let extract_inductive env kn =
   let ind = extract_ind env kn in
diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mlpack
index ad321243..9184f650 100644
--- a/plugins/extraction/extraction_plugin.mllib
+++ b/plugins/extraction/extraction_plugin.mlpack
@@ -9,4 +9,3 @@ Scheme
 Json
 Extract_env
 G_extraction
-Extraction_plugin_mod
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index aec95868..19fda4ae 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -8,9 +8,14 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+DECLARE PLUGIN "extraction_plugin"
+
 (* ML names *)
 
 open Genarg
+open Stdarg
+open Constrarg
+open Pcoq.Prim
 open Pp
 open Names
 open Nameops
@@ -31,7 +36,6 @@ let pr_int_or_id _ _ _ = function
   | ArgId id -> pr_id id
 
 ARGUMENT EXTEND int_or_id
-  TYPED AS int_or_id
   PRINTED BY pr_int_or_id
 | [ preident(id) ] -> [ ArgId (Id.of_string id) ]
 | [ integer(i) ] -> [ ArgInt i ]
@@ -99,7 +103,7 @@ END
 
 VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY
 | [ "Print" "Extraction" "Inline" ]
-  -> [ msg_info (print_extraction_inline ()) ]
+  -> [Feedback. msg_info (print_extraction_inline ()) ]
 END
 
 VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF
@@ -121,7 +125,7 @@ END
 
 VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY
 | [ "Print" "Extraction" "Blacklist" ]
-  -> [ msg_info (print_extraction_blacklist ()) ]
+  -> [ Feedback.msg_info (print_extraction_blacklist ()) ]
 END
 
 VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 22519e34..0692c88c 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -9,7 +9,7 @@
 (*s Production of Haskell syntax. *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
@@ -346,7 +346,7 @@ let pp_decl = function
 	  in
 	  if void then mt ()
 	  else
-	    names.(i) ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () ++
+	    hov 2 (names.(i) ++ str " :: " ++ pp_type false [] typs.(i)) ++ fnl () ++
 	    (if is_custom r then
 		(names.(i) ++ str " = " ++ str (find_custom r))
 	     else
@@ -357,7 +357,7 @@ let pp_decl = function
       if is_inline_custom r then mt ()
       else
 	let e = pp_global Term r in
-	e ++ str " :: " ++ pp_type false [] t ++ fnl () ++
+	hov 2 (e ++ str " :: " ++ pp_type false [] t) ++ fnl () ++
 	  if is_custom r then
 	    hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl2 ())
 	  else
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index df79c585..e43c47d0 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -1,8 +1,6 @@
 open Pp
-open Errors
 open Util
 open Names
-open Nameops
 open Globnames
 open Table
 open Miniml
@@ -18,9 +16,6 @@ let json_int i =
 let json_bool b =
   if b then str "true" else str "false"
 
-let json_null =
-  str "null"
-
 let json_global typ ref =
   json_str (Common.pp_global typ ref)
 
@@ -147,7 +142,8 @@ let rec json_expr env = function
           ("what", json_str "fix:item");
           ("name", json_id fi);
           ("body", json_function env' ti)
-        ]) (Array.map2 (fun a b -> a,b) ids' defs)))
+        ]) (Array.map2 (fun a b -> a,b) ids' defs)));
+      ("for", json_int i);
     ]
   | MLexn s -> json_dict [
       ("what", json_str "expr:exception");
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index b5e8b480..60fe8e76 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -8,7 +8,7 @@
 
 open Names
 open Globnames
-open Errors
+open CErrors
 open Util
 open Miniml
 open Table
@@ -310,7 +310,7 @@ let base_r = function
 let reset_needed, add_needed, add_needed_mp, found_needed, is_needed =
   let needed = ref Refset'.empty
   and needed_mps = ref MPset.empty in
-  ((fun l -> needed := Refset'.empty; needed_mps := MPset.empty),
+  ((fun () -> needed := Refset'.empty; needed_mps := MPset.empty),
    (fun r -> needed := Refset'.add (base_r r) !needed),
    (fun mp -> needed_mps := MPset.add mp !needed_mps),
    (fun r -> needed := Refset'.remove (base_r r) !needed),
@@ -380,14 +380,6 @@ let rec depcheck_struct = function
       let lse' = depcheck_se lse in
       if List.is_empty lse' then struc' else (mp,lse')::struc'
 
-let is_prefix pre s =
-  let len = String.length pre in
-  let rec is_prefix_aux i =
-    if Int.equal i len then true
-    else pre.[i] == s.[i] && is_prefix_aux (succ i)
-  in
-  is_prefix_aux 0
-
 exception RemainingImplicit of kill_reason
 
 let check_for_remaining_implicits struc =
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 3cb3810c..1c29a9bc 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -9,7 +9,7 @@
 (*s Production of Ocaml syntax. *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Nameops
@@ -203,7 +203,7 @@ let rec pp_expr par env args =
 	   let args = List.skipn (projection_arity r) args in
 	   let record = List.hd args in
 	   pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
-	 with e when Errors.noncritical e -> apply (pp_global Term r))
+	 with e when CErrors.noncritical e -> apply (pp_global Term r))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
 	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 7b0f14df..a6309e61 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -9,7 +9,7 @@
 (*s Production of Scheme syntax. *)
 
 open Pp
-open Errors
+open CErrors
 open Util
 open Names
 open Miniml
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index d7842e12..ff66d915 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -15,7 +15,7 @@ open Libobject
 open Goptions
 open Libnames
 open Globnames
-open Errors
+open CErrors
 open Util
 open Pp
 open Miniml
@@ -295,81 +295,94 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref)
 
 let err s = errorlabstrm "Extraction" s
 
+let warn_extraction_axiom_to_realize =
+  CWarnings.create ~name:"extraction-axiom-to-realize" ~category:"extraction"
+         (fun axioms ->
+          let s = if Int.equal (List.length axioms) 1 then "axiom" else "axioms" in
+          strbrk ("The following "^s^" must be realized in the extracted code:")
+                   ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global axioms)
+                   ++ str "." ++ fnl ())
+
+let warn_extraction_logical_axiom =
+  CWarnings.create ~name:"extraction-logical-axiom" ~category:"extraction"
+         (fun axioms ->
+          let s =
+            if Int.equal (List.length axioms) 1 then "axiom was" else "axioms were"
+          in
+          (strbrk ("The following logical "^s^" encountered:") ++
+             hov 1 (spc () ++ prlist_with_sep spc safe_pr_global axioms ++ str ".\n")
+           ++ strbrk "Having invalid logical axiom in the environment when extracting"
+           ++ spc () ++ strbrk "may lead to incorrect or non-terminating ML terms." ++
+             fnl ()))
+
 let warning_axioms () =
   let info_axioms = Refset'.elements !info_axioms in
-  if List.is_empty info_axioms then ()
-  else begin
-    let s = if Int.equal (List.length info_axioms) 1 then "axiom" else "axioms" in
-    msg_warning
-      (str ("The following "^s^" must be realized in the extracted code:")
-       ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
-       ++ str "." ++ fnl ())
-  end;
+  if not (List.is_empty info_axioms) then
+    warn_extraction_axiom_to_realize info_axioms;
   let log_axioms = Refset'.elements !log_axioms in
-  if List.is_empty log_axioms then ()
-  else begin
-    let s = if Int.equal (List.length log_axioms) 1 then "axiom was" else "axioms were"
-    in
-    msg_warning
-      (str ("The following logical "^s^" encountered:") ++
-       hov 1
-         (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n")
-       ++
-       str "Having invalid logical axiom in the environment when extracting" ++
-       spc () ++ str "may lead to incorrect or non-terminating ML terms." ++
-       fnl ())
-  end
+  if not (List.is_empty log_axioms) then
+    warn_extraction_logical_axiom log_axioms
+
+let warn_extraction_opaque_accessed =
+  CWarnings.create ~name:"extraction-opaque-accessed" ~category:"extraction"
+    (fun lst -> strbrk "The extraction is currently set to bypass opacity, " ++
+                  strbrk "the following opaque constant bodies have been accessed :" ++
+                  lst ++ str "." ++ fnl ())
+
+let warn_extraction_opaque_as_axiom =
+  CWarnings.create ~name:"extraction-opaque-as-axiom" ~category:"extraction"
+    (fun lst -> strbrk "The extraction now honors the opacity constraints by default, " ++
+	 strbrk "the following opaque constants have been extracted as axioms :" ++
+	 lst ++ str "." ++ fnl () ++
+	 strbrk "If necessary, use \"Set Extraction AccessOpaque\" to change this."
+	 ++ fnl ())
 
 let warning_opaques accessed =
   let opaques = Refset'.elements !opaques in
-  if List.is_empty opaques then ()
-  else
+  if not (List.is_empty opaques) then
     let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in
-    if accessed then
-      msg_warning
-	(str "The extraction is currently set to bypass opacity,\n" ++
-	 str "the following opaque constant bodies have been accessed :" ++
-	 lst ++ str "." ++ fnl ())
-    else
-      msg_warning
-	(str "The extraction now honors the opacity constraints by default,\n" ++
-	 str "the following opaque constants have been extracted as axioms :" ++
-	 lst ++ str "." ++ fnl () ++
-	 str "If necessary, use \"Set Extraction AccessOpaque\" to change this."
-	 ++ fnl ())
-
-let warning_both_mod_and_cst q mp r =
- msg_warning
-   (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++
-    str "do you mean module " ++
-    pr_long_mp mp ++
-    str " or object " ++
-    pr_long_global r ++ str " ?" ++ fnl () ++
-    str "First choice is assumed, for the second one please use " ++
-    str "fully qualified name." ++ fnl ())
+    if accessed then warn_extraction_opaque_accessed lst
+    else warn_extraction_opaque_as_axiom lst
+
+let warning_ambiguous_name =
+  CWarnings.create ~name:"extraction-ambiguous-name" ~category:"extraction"
+    (fun (q,mp,r) -> strbrk "The name " ++ pr_qualid q ++ strbrk " is ambiguous, " ++
+                       strbrk "do you mean module " ++
+                       pr_long_mp mp ++
+                       strbrk " or object " ++
+                       pr_long_global r ++ str " ?" ++ fnl () ++
+                       strbrk "First choice is assumed, for the second one please use " ++
+                       strbrk "fully qualified name." ++ fnl ())
 
 let error_axiom_scheme r i =
   err (str "The type scheme axiom " ++ spc () ++
        safe_pr_global r ++ spc () ++ str "needs " ++ int i ++
        str " type variable(s).")
 
+let warn_extraction_inside_module =
+  CWarnings.create ~name:"extraction-inside-module" ~category:"extraction"
+      (fun () -> strbrk "Extraction inside an opened module is experimental." ++
+       strbrk "In case of problem, close it first.")
+
+
 let check_inside_module () =
   if Lib.is_modtype () then
     err (str "You can't do that within a Module Type." ++ fnl () ++
 	 str "Close it and try again.")
   else if Lib.is_module () then
-    msg_warning
-      (str "Extraction inside an opened module is experimental.\n" ++
-       str "In case of problem, close it first.\n")
+    warn_extraction_inside_module ()
 
 let check_inside_section () =
   if Lib.sections_are_opened () then
     err (str "You can't do that within a section." ++ fnl () ++
 	 str "Close it and try again.")
 
-let warning_id s =
-  msg_warning (str ("The identifier "^s^
-		    " contains __ which is reserved for the extraction"))
+let warn_extraction_reserved_identifier =
+  CWarnings.create ~name:"extraction-reserved-identifier" ~category:"extraction"
+    (fun s -> strbrk ("The identifier "^s^
+                " contains __ which is reserved for the extraction"))
+
+let warning_id s = warn_extraction_reserved_identifier s
 
 let error_constant r =
   err (safe_pr_global r ++ str " is not a constant.")
@@ -391,9 +404,15 @@ let error_no_module_expr mp =
        ++ str "some Declare Module outside any Module Type.\n"
        ++ str "This situation is currently unsupported by the extraction.")
 
-let error_singleton_become_prop id =
+let error_singleton_become_prop id og =
+  let loc =
+    match og with
+    | Some g -> fnl () ++ str "in " ++ safe_pr_global g ++
+                str " (or in its mutual block)"
+    | None -> mt ()
+  in
   err (str "The informative inductive type " ++ pr_id id ++
-       str " has a Prop instance.\n" ++
+       str " has a Prop instance" ++ loc ++ str "." ++ fnl () ++
        str "This happens when a sort-polymorphic singleton inductive type\n" ++
        str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++
        str "The Ocaml extraction cannot handle this situation yet.\n" ++
@@ -422,7 +441,7 @@ let error_MPfile_as_mod mp b =
 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
+    decompose_prod (Reduction.whd_all (Global.env ()) typ) in
   List.rev_map fst rels
 
 let msg_of_implicit = function
@@ -441,25 +460,28 @@ let error_remaining_implicit k =
        str "You might also try Unset Extraction SafeImplicits to force" ++
        fnl() ++ str "the extraction of unsafe code and review it manually.")
 
+let warn_extraction_remaining_implicit =
+  CWarnings.create ~name:"extraction-remaining-implicit" ~category:"extraction"
+    (fun s -> strbrk ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++
+     strbrk "Extraction SafeImplicits is unset, extracting nonetheless,"
+     ++ strbrk "but this code is potentially unsafe, please 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.")
+  warn_extraction_remaining_implicit s
 
 let check_loaded_modfile mp = match base_mp mp with
   | MPfile dp ->
       if not (Library.library_is_loaded dp) then begin
 	match base_mp (Lib.current_mp ()) with
 	  | MPfile dp' when not (DirPath.equal dp dp') ->
-	      err (str ("Please load library "^(DirPath.to_string dp^" first.")))
+	      err (str "Please load library " ++ pr_dirpath dp ++ str " first.")
 	  | _ -> ()
       end
   | _ -> ()
 
 let info_file f =
-  Flags.if_verbose msg_info
+  Flags.if_verbose Feedback.msg_info
     (str ("The file "^f^" has been created by extraction."))
 
 
@@ -858,7 +880,7 @@ let extract_constant_inline inline r ids s =
     | ConstRef kn ->
 	let env = Global.env () in
 	let typ = Global.type_of_global_unsafe (ConstRef kn) in
-	let typ = Reduction.whd_betadeltaiota env typ in
+	let typ = Reduction.whd_all env typ in
 	if Reduction.is_arity env typ
 	  then begin
 	    let nargs = Hook.get use_type_scheme_nb_args env typ in
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