aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/common.ml40
-rw-r--r--plugins/extraction/extract_env.ml11
-rw-r--r--plugins/extraction/extraction.ml24
-rw-r--r--plugins/extraction/extraction_plugin.mlpack (renamed from plugins/extraction/extraction_plugin.mllib)1
-rw-r--r--plugins/extraction/g_extraction.ml410
-rw-r--r--plugins/extraction/haskell.ml2
-rw-r--r--plugins/extraction/json.ml5
-rw-r--r--plugins/extraction/modutil.ml12
-rw-r--r--plugins/extraction/ocaml.ml4
-rw-r--r--plugins/extraction/scheme.ml2
-rw-r--r--plugins/extraction/table.ml136
-rw-r--r--plugins/extraction/table.mli3
12 files changed, 125 insertions, 125 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index f2e7c3ede1..3c5f6cb720 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -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
@@ -332,12 +333,9 @@ let reset_renaming_tables flag =
let modular_rename k id =
let s = ascii_of_id id in
- let prefix,is_ok =
- if upperkind k then "Coq_",is_upper else "coq_",is_lower
+ 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);
- (Id.to_string nextcoq)^"_"^(ascii_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 = 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 ... *)
@@ -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 41a068ff38..52f22ee603 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 114c5149f6..312c2eab3d 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
@@ -74,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)
@@ -102,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
@@ -135,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
@@ -143,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
@@ -249,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
@@ -489,7 +489,7 @@ and extract_really_ind env kn mib =
*)
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
@@ -573,7 +573,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
@@ -684,7 +684,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
@@ -848,7 +848,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. *)
diff --git a/plugins/extraction/extraction_plugin.mllib b/plugins/extraction/extraction_plugin.mlpack
index ad32124347..9184f65017 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 aec9586895..19fda4aead 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 764223621e..0692c88cd1 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
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index df79c585e5..8874afef33 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)
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index b5e8b48044..60fe8e7620 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 3cb3810cbc..1c29a9bc24 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 7b0f14dff7..a6309e61f9 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 5f83d2949e..ff66d915f5 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.")
@@ -428,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
@@ -447,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."))
@@ -864,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 62c20bd3a7..15a08756c0 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 22:56:40 +0000