aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/extraction/common.ml237
-rw-r--r--plugins/extraction/common.mli4
-rw-r--r--plugins/extraction/extract_env.ml2
-rw-r--r--plugins/extraction/haskell.ml2
-rw-r--r--plugins/extraction/ocaml.ml46
-rw-r--r--plugins/extraction/scheme.ml2
-rw-r--r--plugins/extraction/table.ml24
-rw-r--r--plugins/extraction/table.mli4
8 files changed, 194 insertions, 127 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 0941ed50f..41ce4d2d4 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -20,7 +20,14 @@ open Mlutil
open Modutil
open Mod_subst
-let string_of_id id = ascii_of_ident (Names.string_of_id id)
+let string_of_id id =
+ let s = Names.string_of_id id in
+ for i = 0 to String.length s - 2 do
+ if s.[i] = '_' && s.[i+1] = '_' then warning_id s
+ done;
+ ascii_of_ident s
+
+let is_mp_bound = function MPbound _ -> true | _ -> false
(*s Some pretty-print utility functions. *)
@@ -62,17 +69,14 @@ let unquote s =
for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done;
s
-let rec dottify = function
+let rec qualify delim = function
| [] -> assert false
| [s] -> s
- | s::[""] -> s
- | s::l -> (dottify l)^"."^s
+ | ""::l -> qualify delim l
+ | s::l -> s^delim^(qualify delim l)
-let rec pseudo_qualify up = function
- | [] -> assert false
- | [s] -> s
- | s::[""] -> s
- | s::l -> (if up then "" else "_")^(pseudo_qualify true l)^"__"^s
+let dottify = qualify "."
+let pseudo_qualify = qualify "__"
(*s Uppercase/lowercase renamings. *)
@@ -183,23 +187,34 @@ let mpfiles_add, mpfiles_mem, mpfiles_list, mpfiles_clear =
register_cleanup clear;
(add,mem,list,clear)
+(*s List of module parameters that we should alpha-rename *)
+
+let params_ren_add, params_ren_mem =
+ let m = ref MPset.empty in
+ let add mp = m:=MPset.add mp !m
+ and mem mp = MPset.mem mp !m
+ and clear () = m:=MPset.empty
+ in
+ register_cleanup clear;
+ (add,mem)
+
(*s table indicating the visible horizon at a precise moment,
i.e. the stack of structures we are inside.
- The sequence of [mp] parts should have the following form:
- [X.Y; X; A.B.C; A.B; A; ...], i.e. each addition should either
- be a [MPdot] over the last entry, or something new, mainly
- [MPself], or [MPfile] at the beginning.
+ a [MPfile] at the beginning, and then more and more [MPdot]
+ over this [MPfile].
- - The [content] part is used to recoard all the names already
- seen at this level.
+ - the [params] are the [MPbound] when [mp] is a functor,
+ the innermost [MPbound] coming first in the list.
- - The [subst] part is here mainly for printing signature
- (in which names are still short, i.e. relative to a [msid]).
+ - The [content] part is used to record all the names already
+ seen at this level.
*)
type visible_layer = { mp : module_path;
- content : ((kind*string),unit) Hashtbl.t }
+ params : module_path list;
+ content : ((kind*string),label) Hashtbl.t }
let pop_visible, push_visible, get_visible =
let vis = ref [] in
@@ -210,15 +225,15 @@ let pop_visible, push_visible, get_visible =
if get_phase () = Impl && modular () && is_modfile v.mp
then add_mpfiles_content v.mp v.content;
vis := List.tl !vis
- and push mp =
- vis := { mp = mp; content = Hashtbl.create 97 } :: !vis
+ and push mp mps =
+ vis := { mp = mp; params = mps; content = Hashtbl.create 97 } :: !vis
and get () = !vis
in (pop,push,get)
let get_visible_mps () = List.map (function v -> v.mp) (get_visible ())
let top_visible () = match get_visible () with [] -> assert false | v::_ -> v
let top_visible_mp () = (top_visible ()).mp
-let add_visible ks = Hashtbl.add (top_visible ()).content ks ()
+let add_visible ks l = Hashtbl.add (top_visible ()).content ks l
(* table of local module wrappers used to provide non-ambiguous names *)
@@ -284,7 +299,10 @@ let rec mp_renaming_fun mp = match mp with
let lmp = mp_renaming mp in
if lmp = [""] then (modfstlev_rename l)::lmp
else (modular_rename Mod (id_of_label l))::lmp
- | MPbound mbid -> [modular_rename Mod (id_of_mbid mbid)]
+ | MPbound mbid ->
+ let s = modular_rename Mod (id_of_mbid mbid) in
+ if not (params_ren_mem mp) then [s]
+ else let i,_,_ = repr_mbid mbid in [s^"__"^string_of_int i]
| MPfile _ when not (modular ()) -> assert false (* see [at_toplevel] above *)
| MPfile _ ->
assert (get_phase () = Pre);
@@ -296,7 +314,9 @@ let rec mp_renaming_fun mp = match mp with
and mp_renaming =
let add,get,_ = mktable true in
- fun x -> try get x with Not_found -> let y = mp_renaming_fun x in add x y; y
+ fun x ->
+ try if is_mp_bound (base_mp x) then raise Not_found; get x
+ with Not_found -> let y = mp_renaming_fun x in add x y; y
(*s Renamings creation for a [global_reference]: we build its fully-qualified
name in a [string list] form (head is the short name). *)
@@ -320,7 +340,9 @@ let ref_renaming_fun (k,r) =
let ref_renaming =
let add,get,_ = mktable true in
- fun x -> try get x with Not_found -> let y = ref_renaming_fun x in add x y; y
+ fun x ->
+ try if is_mp_bound (base_mp (modpath_of_r (snd x))) then raise Not_found; get x
+ with Not_found -> let y = ref_renaming_fun x in add x y; y
(* [visible_clash mp0 (k,s)] checks if [mp0-s] of kind [k]
can be printed as [s] in the current context of visible
@@ -338,12 +360,38 @@ let mpfiles_clash mp0 ks =
clash (fun mp -> Hashtbl.mem (get_mpfiles_content mp)) mp0 ks
(List.rev (mpfiles_list ()))
+let rec params_lookup mp0 ks = function
+ | [] -> false
+ | param :: _ when mp0 = param -> true
+ | param :: params ->
+ if ks = (Mod, List.hd (mp_renaming param)) then params_ren_add param;
+ params_lookup mp0 ks params
+
let visible_clash mp0 ks =
let rec clash = function
| [] -> false
| v :: _ when v.mp = mp0 -> false
- | v :: _ when Hashtbl.mem v.content ks -> true
- | _ :: vis -> clash vis
+ | v :: vis ->
+ let b = Hashtbl.mem v.content ks in
+ if b && not (is_mp_bound mp0) then true
+ else begin
+ if b then params_ren_add mp0;
+ if params_lookup mp0 ks v.params then false
+ else clash vis
+ end
+ in clash (get_visible ())
+
+(* Same, but with verbose output (and mp0 shouldn't be a MPbound) *)
+
+let visible_clash_dbg mp0 ks =
+ let rec clash = function
+ | [] -> None
+ | v :: _ when v.mp = mp0 -> None
+ | v :: vis ->
+ try Some (v.mp,Hashtbl.find v.content ks)
+ with Not_found ->
+ if params_lookup mp0 ks v.params then None
+ else clash vis
in clash (get_visible ())
(* After the 1st pass, we can decide which modules will be opened initially *)
@@ -370,81 +418,106 @@ let opened_libraries () =
(* First, a function that factorize the printing of both [global_reference]
and module names for ocaml. When [k=Mod] then [olab=None], otherwise it
contains the label of the reference to print.
- Invariant: [List.length ls >= 2], simpler situations are handled elsewhere. *)
-
-let pp_ocaml_gen k mp ls olab =
- try (* what is the largest prefix of [mp] that belongs to [visible]? *)
- let prefix = common_prefix_from_list mp (get_visible_mps ()) in
- let delta = mp_length mp - mp_length prefix in
- assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *)
- let ls = list_firstn (delta + if k = Mod then 0 else 1) ls in
- let s,ls' = list_sep_last ls in
- (* Reference r / module path mp is of the form [<prefix>.s.<List.rev ls'>].
- Difficulty: in ocaml the prefix part cannot be used for
- qualification (we are inside it) and the rest of the long
- name may be hidden.
- Solution: we duplicate the _definition_ of r / mp in a Coq__XXX module *)
- let k' = if ls' = [] then k else Mod in
- if visible_clash prefix (k',s) then
- let front = if ls' = [] && k <> Mod then [s] else ls' in
- let lab = (* label associated with s *)
- if delta = 0 && k <> Mod then Option.get olab
- else get_nth_label_mp delta mp
- in
- try dottify (front @ [check_duplicate prefix lab])
- with Not_found ->
- assert (get_phase () = Pre); (* otherwise it's too late *)
- add_duplicate prefix lab; dottify ls
- else dottify ls
- with Not_found ->
- (* [mp] belongs to a closed module, not one of [visible]. *)
- let base = base_mp mp in
- let base_s,ls1 = list_sep_last ls in
- let s,ls2 = list_sep_last ls1 in
- (* [List.rev ls] is [base_s :: s :: List.rev ls2] *)
- let k' = if ls2 = [] then k else Mod in
- if modular () && (mpfiles_mem base) &&
- (not (mpfiles_clash base (k',s))) &&
- (not (visible_clash base (k',s)))
- then (* Standard situation of an object in another file: *)
- (* Thanks to the "open" of this file we remove its name *)
- dottify ls1
- else if visible_clash base (Mod,base_s) then
- error_module_clash base_s
- else dottify ls
-
-let pp_haskell_gen k mp ls =
- if not (modular ()) then List.hd ls
- else match List.rev ls with
+ [rls] is the string list giving the qualified name, short name at the end.
+ Invariant: [List.length rls >= 2], simpler situations are handled elsewhere. *)
+
+(* [pp_ocaml_bound] : [mp] starts with a [MPbound] *)
+
+let pp_ocaml_bound k base mp rls olab =
+ (* clash with a MPbound will be detected and fixed by renaming this MPbound *)
+ if get_phase () = Pre then ignore (visible_clash base (Mod,List.hd rls));
+ dottify rls
+
+(* [pp_ocaml_local] : [mp] has something in common with [top_visible ()]
+ but isn't equal to it *)
+
+let pp_ocaml_local k _ mp rls olab =
+ (* what is the largest prefix of [mp] that belongs to [visible]? *)
+ let prefix = common_prefix_from_list mp (get_visible_mps ()) in
+ assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *)
+ let rls = list_skipn (mp_length prefix) rls in
+ let k',s,rls' = match rls with
| [] -> assert false
- | s::ls' ->
- (if base_mp mp <> top_visible_mp () then s ^ "." else "") ^
- (pseudo_qualify (upperkind k) (List.rev ls'))
+ | [s] -> k,s,[]
+ | s::rls' -> Mod,s,rls'
+ in
+ (* Reference r / module path mp is of the form [<prefix>.s.<rls'>].
+ Difficulty: in ocaml the prefix part cannot be used for
+ qualification (we are inside it) and the rest of the long
+ name may be hidden.
+ Solution: we duplicate the _definition_ of r / mp in a Coq__XXX module *)
+ if not (visible_clash prefix (k',s)) then dottify rls
+ else
+ let front = if rls' = [] && k <> Mod then [s] else rls' in
+ let lab = (* label associated with s *)
+ if prefix = mp then Option.get olab (* here k<>Mod, see assert above *)
+ else get_nth_label_mp (mp_length mp - mp_length prefix) mp
+ in
+ try dottify (check_duplicate prefix lab :: front)
+ with Not_found ->
+ assert (get_phase () = Pre); (* otherwise it's too late *)
+ add_duplicate prefix lab; dottify rls
+
+(* [pp_ocaml_extern] : [mp] isn't local, it is defined in another [MPfile]. *)
+
+let pp_ocaml_extern k base _ rls _ =
+ match rls with
+ | [] | [_] -> assert false
+ | base_s :: s :: rls' ->
+ let k' = if rls' = [] then k else Mod in
+ if modular () && (mpfiles_mem base) &&
+ (not (mpfiles_clash base (k',s))) &&
+ (not (visible_clash base (k',s)))
+ then (* Standard situation of an object in another file: *)
+ (* Thanks to the "open" of this file we remove its name *)
+ dottify (s::rls')
+ else match visible_clash_dbg base (Mod,base_s) with
+ | None -> dottify rls
+ | Some (mp,l) -> error_module_clash base (MPdot (mp,l))
+
+let pp_ocaml_gen k mp rls olab =
+ let base = base_mp mp in
+ let is_local = (base = base_mp (top_visible_mp ())) in
+ let pp = match base with
+ | MPdot _ -> assert false
+ | MPbound _ -> pp_ocaml_bound
+ | MPfile _ when is_local -> pp_ocaml_local
+ | MPfile _ -> pp_ocaml_extern
+ in pp k base mp rls olab
+
+let pp_haskell_gen k mp rls = match rls with
+ | [] -> assert false
+ | s::rls' ->
+ (if base_mp mp <> top_visible_mp () then s ^ "." else "") ^
+ (if upperkind k then "" else "_") ^ pseudo_qualify rls'
let pp_global k r =
let ls = ref_renaming (k,r) in
assert (List.length ls > 1);
let s = List.hd ls in
+ let l = label_of_r r in
let mp = modpath_of_r r in
if mp = top_visible_mp () then
(* simpliest situation: definition of r (or use in the same context) *)
(* we update the visible environment *)
- (add_visible (k,s); unquote s)
- else match lang () with
- | Scheme -> unquote s (* no modular Scheme extraction... *)
- | Haskell -> pp_haskell_gen k mp ls
- | Ocaml -> pp_ocaml_gen k mp ls (Some (label_of_r r))
+ (add_visible (k,s) l; unquote s)
+ else
+ let rls = List.rev ls in (* for what come next it's easier this way *)
+ match lang () with
+ | Scheme -> unquote s (* no modular Scheme extraction... *)
+ | Haskell -> if modular () then pp_haskell_gen k mp rls else s
+ | Ocaml -> pp_ocaml_gen k mp rls (Some (label_of_r r))
(* The next function is used only in Ocaml extraction...*)
let pp_module mp =
let ls = mp_renaming mp in
if List.length ls = 1 then dottify ls
else match mp with
- | MPdot (mp0,_) when mp0 = top_visible_mp () ->
+ | MPdot (mp0,l) when mp0 = top_visible_mp () ->
(* simpliest situation: definition of mp (or use in the same context) *)
(* we update the visible environment *)
let s = List.hd ls in
- add_visible (Mod,s); s
- | _ -> pp_ocaml_gen Mod mp ls None
+ add_visible (Mod,s) l; s
+ | _ -> pp_ocaml_gen Mod mp (List.rev ls) None
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 33c14e33a..b992f0557 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -43,7 +43,9 @@ val pp_global : kind -> global_reference -> string
val pp_module : module_path -> string
val top_visible_mp : unit -> module_path
-val push_visible : module_path -> unit
+(* In [push_visible], the [module_path list] corresponds to
+ module parameters, the innermost one coming first in the list *)
+val push_visible : module_path -> module_path list -> unit
val pop_visible : unit -> unit
val check_duplicate : module_path -> label -> string
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 2fca8016c..3210f2f16 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -366,7 +366,7 @@ let print_one_decl struc mp decl =
set_phase Pre;
ignore (d.pp_struct struc);
set_phase Impl;
- push_visible mp;
+ push_visible mp [];
msgnl (d.pp_decl decl);
pop_visible ()
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index ce9fab735..e03c7313a 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -326,7 +326,7 @@ and pp_module_expr = function
let pp_struct =
let pp_sel (mp,sel) =
- push_visible mp;
+ push_visible mp [];
let p = prlist_strict pp_structure_elem sel in
pop_visible (); p
in
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 377648422..ceb2246ad 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -607,8 +607,8 @@ let rec pp_specif = function
pp_alias_spec ren s
with Not_found -> pp_spec s)
| (l,Smodule mt) ->
- let def = pp_module_type mt in
- let def' = pp_module_type mt in
+ let def = pp_module_type [] mt in
+ let def' = pp_module_type [] mt in
let name = pp_modname (MPdot (top_visible_mp (), l)) in
hov 1 (str "module " ++ name ++ str " : " ++ fnl () ++ def) ++
(try
@@ -616,7 +616,7 @@ let rec pp_specif = function
fnl () ++ hov 1 (str ("module "^ren^" : ") ++ fnl () ++ def')
with Not_found -> Pp.mt ())
| (l,Smodtype mt) ->
- let def = pp_module_type mt in
+ let def = pp_module_type [] mt in
let name = pp_modname (MPdot (top_visible_mp (), l)) in
hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
(try
@@ -624,16 +624,16 @@ let rec pp_specif = function
fnl () ++ str ("module type "^ren^" = ") ++ name
with Not_found -> Pp.mt ())
-and pp_module_type = function
+and pp_module_type params = function
| MTident kn ->
pp_modname kn
| MTfunsig (mbid, mt, mt') ->
- let typ = pp_module_type mt in
+ let typ = pp_module_type [] mt in
let name = pp_modname (MPbound mbid) in
- let def = pp_module_type mt' in
+ let def = pp_module_type (MPbound mbid :: params) mt' in
str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
- | MTsig (mp1, sign) ->
- push_visible mp1;
+ | MTsig (mp, sign) ->
+ push_visible mp params;
let l = map_succeed pp_specif sign in
pop_visible ();
str "sig " ++ fnl () ++
@@ -648,9 +648,9 @@ and pp_module_type = function
in
let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l))
in
- push_visible mp_mt;
+ push_visible mp_mt [];
let s =
- pp_module_type mt ++ str " with type " ++
+ pp_module_type [] mt ++ str " with type " ++
pp_global Type r ++ ids
in
pop_visible();
@@ -660,9 +660,9 @@ and pp_module_type = function
let mp_w =
List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl
in
- push_visible mp_mt;
+ push_visible mp_mt [];
let s =
- pp_module_type mt ++ str " with module " ++ pp_modname mp_w
+ pp_module_type [] mt ++ str " with module " ++ pp_modname mp_w
in
pop_visible ();
s ++ str " = " ++ pp_modname mp
@@ -681,10 +681,10 @@ let rec pp_structure_elem = function
let typ =
(* virtual printing of the type, in order to have a correct mli later*)
if Common.get_phase () = Pre then
- str ": " ++ pp_module_type m.ml_mod_type
+ str ": " ++ pp_module_type [] m.ml_mod_type
else mt ()
in
- let def = pp_module_expr m.ml_mod_expr in
+ let def = pp_module_expr [] m.ml_mod_expr in
let name = pp_modname (MPdot (top_visible_mp (), l)) in
hov 1
(str "module " ++ name ++ typ ++ str " = " ++
@@ -694,7 +694,7 @@ let rec pp_structure_elem = function
fnl () ++ str ("module "^ren^" = ") ++ name
with Not_found -> mt ())
| (l,SEmodtype m) ->
- let def = pp_module_type m in
+ let def = pp_module_type [] m in
let name = pp_modname (MPdot (top_visible_mp (), l)) in
hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
(try
@@ -702,17 +702,17 @@ let rec pp_structure_elem = function
fnl () ++ str ("module type "^ren^" = ") ++ name
with Not_found -> mt ())
-and pp_module_expr = function
- | MEident mp' -> pp_modname mp'
+and pp_module_expr params = function
+ | MEident mp -> pp_modname mp
+ | MEapply (me, me') ->
+ pp_module_expr [] me ++ str "(" ++ pp_module_expr [] me' ++ str ")"
| MEfunctor (mbid, mt, me) ->
let name = pp_modname (MPbound mbid) in
- let typ = pp_module_type mt in
- let def = pp_module_expr me in
+ let typ = pp_module_type [] mt in
+ let def = pp_module_expr (MPbound mbid :: params) me in
str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
- | MEapply (me, me') ->
- pp_module_expr me ++ str "(" ++ pp_module_expr me' ++ str ")"
| MEstruct (mp, sel) ->
- push_visible mp;
+ push_visible mp params;
let l = map_succeed pp_structure_elem sel in
pop_visible ();
str "struct " ++ fnl () ++
@@ -723,7 +723,7 @@ let do_struct f s =
let pp s = try f s ++ fnl2 () with Failure "empty phrase" -> mt ()
in
let ppl (mp,sel) =
- push_visible mp;
+ push_visible mp [];
let p = prlist_strict pp sel in
(* for monolithic extraction, we try to simulate the unavailability
of [MPfile] in names by artificially nesting these [MPfile] *)
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 9c600760f..64b86e6e2 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -195,7 +195,7 @@ and pp_module_expr = function
let pp_struct =
let pp_sel (mp,sel) =
- push_visible mp;
+ push_visible mp [];
let p = prlist_strict pp_structure_elem sel in
pop_visible (); p
in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index a380654c6..6691e2622 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -82,7 +82,7 @@ let rec get_nth_label_mp n = function
let common_prefix_from_list mp0 mpl =
let prefixes = prefixes_mp mp0 in
let rec f = function
- | [] -> raise Not_found
+ | [] -> assert false
| mp :: l -> if MPset.mem mp prefixes then mp else f l
in f mpl
@@ -108,19 +108,6 @@ let labels_of_ref r =
in
parse_labels2 [l] mp_top mp
-
-
-
-let labels_of_ref2 r =
- let mp1,_,l =
- match r with
- ConstRef con -> repr_con con
- | IndRef (kn,_)
- | ConstructRef ((kn,_),_) -> repr_mind kn
- | VarRef _ -> assert false
- in mp1,l
-
-
let rec add_labels_mp mp = function
| [] -> mp
| l :: ll -> add_labels_mp (MPdot (mp,l)) ll
@@ -287,6 +274,10 @@ let check_inside_section () =
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 error_constant r =
err (safe_pr_global r ++ str " is not a constant.")
@@ -296,8 +287,9 @@ let error_inductive r =
let error_nb_cons () =
err (str "Not the right number of constructors.")
-let error_module_clash s =
- err (str ("There are two Coq modules with ML name " ^ s ^".\n") ++
+let error_module_clash mp1 mp2 =
+ err (str "The Coq modules " ++ pr_long_mp mp1 ++ str " and " ++
+ pr_long_mp mp2 ++ str " have the same ML name.\n" ++
str "This is not supported yet. Please do some renaming first.")
let error_unknown_module m =
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index b215e373e..e64f1de15 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -18,11 +18,12 @@ val safe_basename_of_global : global_reference -> identifier
val warning_axioms : unit -> unit
val warning_both_mod_and_cst :
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
val error_inductive : global_reference -> 'a
val error_nb_cons : unit -> 'a
-val error_module_clash : string -> 'a
+val error_module_clash : module_path -> module_path -> 'a
val error_unknown_module : qualid -> 'a
val error_scheme : unit -> 'a
val error_not_visible : global_reference -> 'a
@@ -56,7 +57,6 @@ val common_prefix_from_list : module_path -> module_path list -> module_path
val add_labels_mp : module_path -> label list -> module_path
val get_nth_label_mp : int -> module_path -> label
val labels_of_ref : global_reference -> module_path * label list
-val labels_of_ref2 : global_reference -> module_path * label
(*s Some table-related operations *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 03:34:11 +0000