aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/common.ml1
-rw-r--r--plugins/extraction/common.mli24
-rw-r--r--plugins/extraction/extract_env.ml85
-rw-r--r--plugins/extraction/extract_env.mli7
-rw-r--r--plugins/extraction/extraction.ml15
-rw-r--r--plugins/extraction/extraction.mli1
-rw-r--r--plugins/extraction/g_extraction.ml47
-rw-r--r--plugins/extraction/haskell.ml1
-rw-r--r--plugins/extraction/json.ml1
-rw-r--r--plugins/extraction/miniml.mli16
-rw-r--r--plugins/extraction/mlutil.ml3
-rw-r--r--plugins/extraction/mlutil.mli1
-rw-r--r--plugins/extraction/modutil.ml10
-rw-r--r--plugins/extraction/modutil.mli2
-rw-r--r--plugins/extraction/ocaml.ml1
-rw-r--r--plugins/extraction/scheme.ml1
-rw-r--r--plugins/extraction/table.ml8
-rw-r--r--plugins/extraction/table.mli5
18 files changed, 115 insertions, 74 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 19ba31fbbd..9772ebd641 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Pp
open Util
open Names
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 28a7c4d457..356bad98ba 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -6,34 +6,32 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Names
open Globnames
open Miniml
-open Pp
(** By default, in module Format, you can do horizontal placing of blocks
even if they include newlines, as long as the number of chars in the
blocks are less that a line length. To avoid this awkward situation,
we attach a big virtual size to [fnl] newlines. *)
-val fnl : unit -> std_ppcmds
-val fnl2 : unit -> std_ppcmds
-val space_if : bool -> std_ppcmds
+val fnl : unit -> Pp.t
+val fnl2 : unit -> Pp.t
+val space_if : bool -> Pp.t
-val pp_par : bool -> std_ppcmds -> std_ppcmds
+val pp_par : bool -> Pp.t -> Pp.t
(** [pp_apply] : a head part applied to arguments, possibly with parenthesis *)
-val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
+val pp_apply : Pp.t -> bool -> Pp.t list -> Pp.t
(** Same as [pp_apply], but with also protection of the head by parenthesis *)
-val pp_apply2 : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
+val pp_apply2 : Pp.t -> bool -> Pp.t list -> Pp.t
-val pp_tuple_light : (bool -> 'a -> std_ppcmds) -> 'a list -> std_ppcmds
-val pp_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
-val pp_boxed_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val pp_tuple_light : (bool -> 'a -> Pp.t) -> 'a list -> Pp.t
+val pp_tuple : ('a -> Pp.t) -> 'a list -> Pp.t
+val pp_boxed_tuple : ('a -> Pp.t) -> 'a list -> Pp.t
-val pr_binding : Id.t list -> std_ppcmds
+val pr_binding : Id.t list -> Pp.t
val rename_id : Id.t -> Id.Set.t -> Id.t
@@ -81,4 +79,4 @@ val mk_ind : string -> string -> MutInd.t
val is_native_char : ml_ast -> bool
val get_native_char : ml_ast -> char
-val pp_native_char : ml_ast -> std_ppcmds
+val pp_native_char : ml_ast -> Pp.t
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 79d602dbe8..89c2a0ae30 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Miniml
open Term
open Declarations
@@ -133,7 +132,7 @@ let rec add_labels mp = function
exception Impossible
let check_arity env cb =
- let t = Typeops.type_of_constant_type env cb.const_type in
+ let t = cb.const_type in
if Reduction.is_arity env t then raise Impossible
let check_fix env cb i =
@@ -176,26 +175,32 @@ let factor_fix env l cb msb =
(hack proposed by Elie)
*)
-let expand_mexpr env mp me =
+let expand_mexpr env mpo me =
let inl = Some (Flags.get_inline_level()) in
- Mod_typing.translate_mse env (Some mp) inl me
+ Mod_typing.translate_mse env mpo inl me
-(** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def].
- To check with Elie. *)
-
-let rec mp_of_mexpr = function
- | MEident mp -> mp
- | MEwith (seb,_) -> mp_of_mexpr seb
- | _ -> assert false
+let expand_modtype env mp me =
+ let inl = Some (Flags.get_inline_level()) in
+ Mod_typing.translate_modtype env mp inl ([],me)
let no_delta = Mod_subst.empty_delta_resolver
-let env_for_mtb_with_def env mp me idl =
+let flatten_modtype env mp me_alg struc_opt =
+ match struc_opt with
+ | Some me -> me, no_delta
+ | None ->
+ let mtb = expand_modtype env mp me_alg in
+ mtb.mod_type, mtb.mod_delta
+
+(** Ad-hoc update of environment, inspired by [Mod_typing.check_with_aux_def].
+*)
+
+let env_for_mtb_with_def env mp me reso idl =
let struc = Modops.destr_nofunctor me in
let l = Label.of_id (List.hd idl) in
let spot = function (l',SFBconst _) -> Label.equal l l' | _ -> false in
let before = fst (List.split_when spot struc) in
- Modops.add_structure mp before no_delta env
+ Modops.add_structure mp before reso env
let make_cst resolver mp l =
Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp l)
@@ -235,20 +240,24 @@ let rec extract_structure_spec env mp reso = function
[extract_mexpression_spec] should come from a [mod_type_alg] field.
This way, any encountered [MEident] should be a true module type. *)
-and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with
+and extract_mexpr_spec env mp1 (me_struct_o,me_alg) = match me_alg with
| MEident mp -> Visit.add_mp_all mp; MTident mp
| MEwith(me',WithDef(idl,(c,ctx)))->
- let env' = env_for_mtb_with_def env (mp_of_mexpr me') me_struct idl in
- let mt = extract_mexpr_spec env mp1 (me_struct,me') in
+ let me_struct,delta = flatten_modtype env mp1 me' me_struct_o in
+ let env' = env_for_mtb_with_def env mp1 me_struct delta idl in
+ let mt = extract_mexpr_spec env mp1 (None,me') in
(match extract_with_type env' c with (* cb may contain some kn *)
| None -> mt
- | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ)))
+ | Some (vl,typ) ->
+ type_iter_references Visit.add_ref typ;
+ MTwith(mt,ML_With_type(idl,vl,typ)))
| MEwith(me',WithMod(idl,mp))->
Visit.add_mp_all mp;
- MTwith(extract_mexpr_spec env mp1 (me_struct,me'), ML_With_module(idl,mp))
+ MTwith(extract_mexpr_spec env mp1 (None,me'), ML_With_module(idl,mp))
| MEapply _ ->
(* No higher-order module type in OCaml : we use the expanded version *)
- extract_msignature_spec env mp1 no_delta (*TODO*) me_struct
+ let me_struct,delta = flatten_modtype env mp1 me_alg me_struct_o in
+ extract_msignature_spec env mp1 delta me_struct
and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with
| MoreFunctor (mbid, mtb, me_alg') ->
@@ -259,8 +268,8 @@ and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with
let mp = MPbound mbid in
let env' = Modops.add_module_type mp mtb env in
MTfunsig (mbid, extract_mbody_spec env mp mtb,
- extract_mexpression_spec env' mp1 (me_struct',me_alg'))
- | NoFunctor m -> extract_mexpr_spec env mp1 (me_struct,m)
+ extract_mexpression_spec env' mp1 (me_struct',me_alg'))
+ | NoFunctor m -> extract_mexpr_spec env mp1 (Some me_struct,m)
and extract_msignature_spec env mp1 reso = function
| NoFunctor struc ->
@@ -336,7 +345,7 @@ and extract_mexpr env mp = function
(* In Haskell/Scheme, we expand everything.
For now, we also extract everything, dead code will be removed later
(see [Modutil.optimize_struct]. *)
- let sign,_,delta,_ = expand_mexpr env mp me in
+ let sign,_,delta,_ = expand_mexpr env (Some mp) me in
extract_msignature env mp delta ~all:true sign
| MEident mp ->
if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
@@ -686,3 +695,35 @@ let structure_for_compute c =
let struc = optimize_struct (refs,[]) (mono_environment refs []) in
let flatstruc = List.map snd (List.flatten (List.map snd struc)) in
flatstruc, ast, mlt
+
+(* For the test-suite :
+ extraction to a temporary file + run ocamlc on it *)
+
+let compile f =
+ try
+ let args = ["ocamlc";"-I";Filename.dirname f;"-c";f^"i";f] in
+ let res = CUnix.sys_command (Envars.ocamlfind ()) args in
+ match res with
+ | Unix.WEXITED 0 -> ()
+ | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n ->
+ CErrors.user_err
+ Pp.(str "Compilation of file " ++ str f ++
+ str " failed with exit code " ++ int n)
+ with Unix.Unix_error (e,_,_) ->
+ CErrors.user_err
+ Pp.(str "Compilation of file " ++ str f ++
+ str " failed with error " ++ str (Unix.error_message e))
+
+let remove f =
+ if Sys.file_exists f then Sys.remove f
+
+let extract_and_compile l =
+ if lang () != Ocaml then
+ CErrors.user_err (Pp.str "This command only works with OCaml extraction");
+ let f = Filename.temp_file "testextraction" ".ml" in
+ let () = full_extraction (Some f) l in
+ let () = compile f in
+ let () = remove f; remove (f^"i") in
+ let base = Filename.chop_suffix f ".ml" in
+ let () = remove (base^".cmo"); remove (base^".cmi") in
+ Feedback.msg_notice (str "Extracted code successfully compiled")
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 0629a84a03..5769ff1176 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -8,7 +8,6 @@
(*s This module declares the extraction commands. *)
-open API
open Names
open Libnames
open Globnames
@@ -18,6 +17,10 @@ val full_extraction : string option -> reference list -> unit
val separate_extraction : reference list -> unit
val extraction_library : bool -> Id.t -> unit
+(* For the test-suite : extraction to a temporary file + ocamlc on it *)
+
+val extract_and_compile : reference list -> unit
+
(* For debug / external output via coqtop.byte + Drop : *)
val mono_environment :
@@ -26,7 +29,7 @@ val mono_environment :
(* Used by the Relation Extraction plugin *)
val print_one_decl :
- Miniml.ml_structure -> ModPath.t -> Miniml.ml_decl -> Pp.std_ppcmds
+ Miniml.ml_structure -> ModPath.t -> Miniml.ml_decl -> Pp.t
(* Used by Extraction Compute *)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index d638c232bb..7644b49ceb 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -7,7 +7,6 @@
(************************************************************************)
(*i*)
-open API
open Util
open Names
open Term
@@ -296,7 +295,11 @@ 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 _ | Proj _ -> Tunknown
+ | Proj (p,t) ->
+ (* Let's try to reduce, if it hasn't already been done. *)
+ if Projection.unfolded p then Tunknown
+ else extract_type env db j (Term.mkProj (Projection.unfold p, t)) args
+ | Case _ | Fix _ | CoFix _ -> Tunknown
| _ -> assert false
(*s Auxiliary function dealing with type application.
@@ -519,7 +522,7 @@ and mlt_env env r = match r with
match lookup_typedef kn cb with
| Some _ as o -> o
| None ->
- let typ = Typeops.type_of_constant_type env cb.const_type
+ let typ = cb.const_type
(* FIXME not sure if we should instantiate univs here *) in
match flag_of_type env typ with
| Info,TypeScheme ->
@@ -544,7 +547,7 @@ let record_constant_type env kn opt_typ =
| Some schema -> schema
| None ->
let typ = match opt_typ with
- | None -> Typeops.type_of_constant_type env cb.const_type
+ | None -> cb.const_type
| Some typ -> typ
in
let mlt = extract_type env [] 1 typ [] in
@@ -970,7 +973,7 @@ let extract_fixpoint env vkn (fi,ti,ci) =
let extract_constant env kn cb =
let r = ConstRef kn in
- let typ = Typeops.type_of_constant_type env cb.const_type in
+ let typ = cb.const_type in
let warn_info () = if not (is_custom r) then add_info_axiom r in
let warn_log () = if not (constant_has_body cb) then add_log_axiom r
in
@@ -1026,7 +1029,7 @@ let extract_constant env kn cb =
let extract_constant_spec env kn cb =
let r = ConstRef kn in
- let typ = Typeops.type_of_constant_type env cb.const_type in
+ let typ = cb.const_type in
try
match flag_of_type env typ with
| (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 5ee34103c5..e1d43f3405 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -8,7 +8,6 @@
(*s Extraction from Coq terms to Miniml. *)
-open API
open Names
open Term
open Declarations
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 2fa453e533..23452febdc 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -8,8 +8,7 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open API
-open Grammar_API.Pcoq.Prim
+open Pcoq.Prim
DECLARE PLUGIN "extraction_plugin"
@@ -66,6 +65,10 @@ VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY
(* Monolithic extraction to a file *)
| [ "Extraction" string(f) ne_global_list(l) ]
-> [ full_extraction (Some f) l ]
+
+(* Extraction to a temporary file and OCaml compilation *)
+| [ "Extraction" "TestCompile" ne_global_list(l) ]
+ -> [ extract_and_compile l ]
END
VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 6146f32bbe..0f537abece 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -8,7 +8,6 @@
(*s Production of Haskell syntax. *)
-open API
open Pp
open CErrors
open Util
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index 1bf19f186b..e43c47d050 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -1,4 +1,3 @@
-open API
open Pp
open Util
open Names
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index ea966baee6..edebba49df 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -8,8 +8,6 @@
(*s Target language for extraction: a core ML called MiniML. *)
-open API
-open Pp
open Names
open Globnames
@@ -206,19 +204,19 @@ type language_descr = {
file_naming : ModPath.t -> string;
(* the second argument is a comment to add to the preamble *)
preamble :
- Id.t -> std_ppcmds option -> ModPath.t list -> unsafe_needs ->
- std_ppcmds;
- pp_struct : ml_structure -> std_ppcmds;
+ Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs ->
+ Pp.t;
+ pp_struct : ml_structure -> Pp.t;
(* Concerning a possible interface file *)
sig_suffix : string option;
(* the second argument is a comment to add to the preamble *)
sig_preamble :
- Id.t -> std_ppcmds option -> ModPath.t list -> unsafe_needs ->
- std_ppcmds;
- pp_sig : ml_signature -> std_ppcmds;
+ Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs ->
+ Pp.t;
+ pp_sig : ml_signature -> Pp.t;
(* for an isolated declaration print *)
- pp_decl : ml_decl -> std_ppcmds;
+ pp_decl : ml_decl -> Pp.t;
}
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index f8c846725e..a4c2bcd883 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -7,7 +7,6 @@
(************************************************************************)
(*i*)
-open API
open Util
open Names
open Libnames
@@ -121,7 +120,6 @@ let rec mgu = function
mgu (a, a'); mgu (b, b')
| Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' ->
List.iter mgu (List.combine l l')
- | (Tdummy _, _ | _, Tdummy _) when lang() == Haskell -> ()
| Tdummy _, Tdummy _ -> ()
| Tvar i, Tvar j when Int.equal i j -> ()
| Tvar' i, Tvar' j when Int.equal i j -> ()
@@ -1053,6 +1051,7 @@ let rec simpl o = function
| MLmagic(MLcase(typ,e,br)) ->
let br' = Array.map (fun (ids,p,c) -> (ids,p,MLmagic c)) br in
simpl o (MLcase(typ,e,br'))
+ | MLmagic(MLdummy _ as e) when lang () == Haskell -> e
| MLmagic(MLexn _ as e) -> e
| a -> ast_map (simpl o) a
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 1db96413a8..42d22a7b45 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Names
open Globnames
open Miniml
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 365dc191ab..1e0c331901 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Names
open ModPath
open Globnames
@@ -18,10 +17,15 @@ open Mlutil
(*S Functions upon ML modules. *)
+(** Note: a syntax like [(F M) with ...] is actually legal, see for instance
+ bug #4720. Hence the code below tries to handle [MTsig], maybe not in
+ a perfect way, but that should be enough for the use of [se_iter] below. *)
+
let rec msid_of_mt = function
| MTident mp -> mp
+ | MTsig(mp,_) -> mp
| MTwith(mt,_)-> msid_of_mt mt
- | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name.")
+ | MTfunsig _ -> assert false (* A functor cannot be inside a MTwith *)
(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
[ml_structure]. *)
@@ -37,7 +41,7 @@ let se_iter do_decl do_spec do_mp =
List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
in
let r = ConstRef (Constant.make2 mp_w (Label.of_id l')) in
- mt_iter mt; do_decl (Dtype(r,l,t))
+ mt_iter mt; do_spec (Stype(r,l,Some t))
| MTwith (mt,ML_With_module(idl,mp))->
let mp_mt = msid_of_mt mt in
let mp_w =
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index 1d9db3a5fc..17a6e8db6f 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Names
open Globnames
open Miniml
@@ -18,6 +17,7 @@ val struct_type_search : (ml_type -> bool) -> ml_structure -> bool
type do_ref = global_reference -> unit
+val type_iter_references : do_ref -> ml_type -> unit
val ast_iter_references : do_ref -> do_ref -> do_ref -> ml_ast -> unit
val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit
val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 2ac411d06f..9cbc3fd713 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -8,7 +8,6 @@
(*s Production of Ocaml syntax. *)
-open API
open Pp
open CErrors
open Util
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index bb96489ab0..1ccc273704 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -8,7 +8,6 @@
(*s Production of Scheme syntax. *)
-open API
open Pp
open CErrors
open Util
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 2642aeefa4..ca98f07e8d 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Names
open ModPath
open Term
@@ -445,9 +444,10 @@ let error_MPfile_as_mod mp b =
"Please "^s2^"use (Recursive) Extraction Library instead.\n"))
let argnames_of_global r =
- let typ = Global.type_of_global_unsafe r in
+ let env = Global.env () in
+ let typ, _ = Global.type_of_global_in_context env r in
let rels,_ =
- decompose_prod (Reduction.whd_all (Global.env ()) typ) in
+ decompose_prod (Reduction.whd_all env typ) in
List.rev_map fst rels
let msg_of_implicit = function
@@ -878,7 +878,7 @@ let extract_constant_inline inline r ids s =
match g with
| ConstRef kn ->
let env = Global.env () in
- let typ = Global.type_of_global_unsafe (ConstRef kn) in
+ let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in
let typ = Reduction.whd_all env typ in
if Reduction.is_arity env typ
then begin
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 0215aa8e48..7e47d0bc81 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Names
open Libnames
open Globnames
@@ -192,7 +191,7 @@ val find_custom_match : ml_branch array -> string
val extraction_language : lang -> unit
val extraction_inline : bool -> reference list -> unit
-val print_extraction_inline : unit -> Pp.std_ppcmds
+val print_extraction_inline : unit -> Pp.t
val reset_extraction_inline : unit -> unit
val extract_constant_inline :
bool -> reference -> string list -> string -> unit
@@ -207,7 +206,7 @@ val extraction_implicit : reference -> int_or_id list -> unit
val extraction_blacklist : Id.t list -> unit
val reset_extraction_blacklist : unit -> unit
-val print_extraction_blacklist : unit -> Pp.std_ppcmds
+val print_extraction_blacklist : unit -> Pp.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 22:49:42 +0000