aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-25 18:19:21 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-25 18:19:21 +0000
commit693d398b5e4e55a916bbdaa8e4c23c83d9dbcef7 (patch)
treee015dc24293114d03433c2cf4412b4fa5df9b87c
parent217bbf499dc09f11a137fdc9aead1e0a78c760c2 (diff)
Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisation (add_glob* et dump_*)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11177 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile.common4
-rw-r--r--contrib/subtac/subtac.ml3
-rw-r--r--contrib/subtac/subtac_classes.ml2
-rw-r--r--interp/constrintern.ml164
-rw-r--r--interp/constrintern.mli7
-rw-r--r--interp/dumpglob.ml220
-rw-r--r--interp/modintern.ml32
-rw-r--r--interp/modintern.mli3
-rw-r--r--kernel/names.ml4
-rw-r--r--kernel/names.mli3
-rw-r--r--lib/flags.ml17
-rw-r--r--lib/flags.mli3
-rw-r--r--library/lib.ml113
-rw-r--r--library/lib.mli127
-rw-r--r--library/library.ml32
-rw-r--r--tactics/auto.ml2
-rw-r--r--tools/coqdoc/index.mll13
-rw-r--r--tools/coqdoc/output.ml18
-rw-r--r--tools/coqdoc/pretty.mll2
-rw-r--r--toplevel/classes.ml2
-rw-r--r--toplevel/coqtop.ml8
-rw-r--r--toplevel/vernac.ml13
-rw-r--r--toplevel/vernacentries.ml170
23 files changed, 491 insertions, 471 deletions
diff --git a/Makefile.common b/Makefile.common
index f31b60a58..c0584b29c 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -172,7 +172,7 @@ PRETYPING:=\
INTERP:=\
parsing/lexer.cmo interp/topconstr.cmo interp/ppextend.cmo \
- interp/notation.cmo \
+ interp/notation.cmo interp/dumpglob.cmo \
interp/genarg.cmo interp/syntax_def.cmo interp/reserve.cmo \
library/impargs.cmo interp/implicit_quantifiers.cmo interp/constrintern.cmo \
interp/modintern.cmo interp/constrextern.cmo interp/coqlib.cmo \
@@ -509,7 +509,7 @@ PRINTERSCMO:=\
pretyping/unification.cmo pretyping/cases.cmo \
pretyping/pretyping.cmo pretyping/clenv.cmo pretyping/pattern.cmo \
parsing/lexer.cmo interp/ppextend.cmo interp/genarg.cmo \
- interp/topconstr.cmo interp/notation.cmo interp/reserve.cmo \
+ interp/topconstr.cmo interp/notation.cmo interp/dumpglob.cmo interp/reserve.cmo \
library/impargs.cmo interp/constrextern.cmo \
interp/syntax_def.cmo interp/implicit_quantifiers.cmo interp/constrintern.cmo \
proofs/proof_trees.cmo proofs/logic.cmo proofs/refiner.cmo \
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 5ac428f6c..71aa7e99e 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -107,7 +107,8 @@ let declare_assumption env isevars idl is_coe k bl c nl =
(str "Cannot declare an assumption while in proof editing mode.")
let dump_definition (loc, id) s =
- Flags.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) (string_of_id id))
+ Dumpglob.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc))
+ (string_of_id id))
let dump_constraint ty ((loc, n), _, _) =
match n with
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index aa16bd4bb..26cb416ac 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -165,7 +165,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
try
let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
- Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
+ Dumpglob.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
c :: props, rest'
with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
([], props) k.cl_props
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1ddcac276..54abacaf6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -124,150 +124,6 @@ let error_inductive_parameter_not_implicit loc =
"the 'return' clauses; they must be replaced by '_' in the 'in' clauses."))
(**********************************************************************)
-(* Dump of globalization (to be used by coqdoc) *)
-let token_number = ref 0
-let last_pos = ref 0
-
-type coqdoc_state = Lexer.location_table * int * int
-
-let coqdoc_freeze () =
- let lt = Lexer.location_table() in
- let state = (lt,!token_number,!last_pos) in
- token_number := 0;
- last_pos := 0;
- state
-
-let coqdoc_unfreeze (lt,tn,lp) =
- Lexer.restore_location_table lt;
- token_number := tn;
- last_pos := lp
-
-open Decl_kinds
-
-let type_of_logical_kind = function
- | IsDefinition def ->
- (match def with
- | Definition -> "def"
- | Coercion -> "coe"
- | SubClass -> "subclass"
- | CanonicalStructure -> "canonstruc"
- | Example -> "ex"
- | Fixpoint -> "def"
- | CoFixpoint -> "def"
- | Scheme -> "scheme"
- | StructureComponent -> "proj"
- | IdentityCoercion -> "coe"
- | Instance -> "inst"
- | Method -> "meth")
- | IsAssumption a ->
- (match a with
- | Definitional -> "defax"
- | Logical -> "prfax"
- | Conjectural -> "prfax")
- | IsProof th ->
- (match th with
- | Theorem
- | Lemma
- | Fact
- | Remark
- | Property
- | Proposition
- | Corollary -> "thm")
-
-let type_of_global_ref gr =
- if Typeclasses.is_class gr then
- "class"
- else
- match gr with
- | ConstRef cst ->
- type_of_logical_kind (Decls.constant_kind cst)
- | VarRef v ->
- "var" ^ type_of_logical_kind (Decls.variable_kind v)
- | IndRef ind ->
- let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
- if mib.Declarations.mind_record then
- if mib.Declarations.mind_finite then "rec"
- else "corec"
- else if mib.Declarations.mind_finite then "ind"
- else "coind"
- | ConstructRef _ -> "constr"
-
-let remove_sections dir =
- if is_dirpath_prefix_of dir (Lib.cwd ()) then
- (* Not yet (fully) discharged *)
- extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
- else
- (* Theorem/Lemma outside its outer section of definition *)
- dir
-
-let dump_reference loc filepath modpath ident ty =
- dump_string (Printf.sprintf "R%d %s %s %s %s\n"
- (fst (unloc loc)) filepath modpath ident ty)
-
-let add_glob_gen loc sp lib_dp ty =
- let mod_dp,id = repr_path sp in
- let mod_dp = remove_sections mod_dp in
- let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in
- let filepath = string_of_dirpath lib_dp in
- let modpath = string_of_dirpath mod_dp_trunc in
- let ident = string_of_id id in
- dump_reference loc filepath modpath ident ty
-
-let add_glob loc ref =
- let sp = Nametab.sp_of_global ref in
- let lib_dp = Lib.library_part ref in
- let ty = type_of_global_ref ref in
- add_glob_gen loc sp lib_dp ty
-
-let add_glob loc ref =
- if !Flags.dump && loc <> dummy_loc then add_glob loc ref
-
-let mp_of_kn kn =
- let mp,sec,l = repr_kn kn in
- MPdot (mp,l)
-
-let add_glob_kn loc kn =
- let sp = Nametab.sp_of_syntactic_definition kn in
- let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
- add_glob_gen loc sp lib_dp "syndef"
-
-let add_glob_kn loc ref =
- if !Flags.dump && loc <> dummy_loc then add_glob_kn loc ref
-
-let add_local loc id = ()
-(* let mod_dp,id = repr_path sp in *)
-(* let mod_dp = remove_sections mod_dp in *)
-(* let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in *)
-(* let filepath = string_of_dirpath lib_dp in *)
-(* let modpath = string_of_dirpath mod_dp_trunc in *)
-(* let ident = string_of_id id in *)
-(* dump_string (Printf.sprintf "R%d %s %s %s %s\n" *)
-(* (fst (unloc loc)) filepath modpath ident ty) *)
-
-let dump_binding loc id = ()
-
-let loc_of_notation f loc args ntn =
- if args=[] or ntn.[0] <> '_' then fst (unloc loc)
- else snd (unloc (f (List.hd args)))
-
-let ntn_loc = loc_of_notation constr_loc
-let patntn_loc = loc_of_notation cases_pattern_expr_loc
-
-let dump_notation_location pos ((path,df),sc) =
- let rec next growing =
- let loc = Lexer.location_function !token_number in
- let (bp,_) = unloc loc in
- if growing then if bp >= pos then loc else (incr token_number;next true)
- else if bp = pos then loc
- else if bp > pos then (decr token_number;next false)
- else (incr token_number;next true) in
- let loc = next (pos >= !last_pos) in
- last_pos := pos;
- let path = string_of_dirpath path in
- let _sc = match sc with Some sc -> " "^sc | None -> "" in
- dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (unloc loc)) path df)
-
-(**********************************************************************)
(* Contracting "{ _ }" in notations *)
let rec wildcards ntn n =
@@ -394,9 +250,9 @@ let rec subst_aconstr_in_rawconstr loc interp subst (renaming,(ids,_,scopes)) =
let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
let ntn,args = contract_notation ntn args in
let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
- if !dump then dump_notation_location (ntn_loc loc args ntn) df;
- let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
- subst_aconstr_in_rawconstr loc intern subst ([],env) c
+ if !Flags.dump then Dumpglob.dump_notation_location (Dumpglob.ntn_loc loc args ntn) df;
+ let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
+ subst_aconstr_in_rawconstr loc intern subst ([],env) c
let set_type_scope (ids,tmp_scope,scopes) =
(ids,Some Notation.type_scope,scopes)
@@ -476,10 +332,10 @@ let check_no_explicitation l =
let intern_qualid loc qid intern env args =
try match Nametab.extended_locate qid with
| TrueGlobal ref ->
- add_glob loc ref;
+ Dumpglob.add_glob loc ref;
RRef (loc, ref), args
| SyntacticDef sp ->
- add_glob_kn loc sp;
+ Dumpglob.add_glob_kn loc sp;
let (ids,c) = Syntax_def.search_syntactic_definition loc sp in
let nids = List.length ids in
if List.length args < nids then error_not_enough_arguments loc;
@@ -709,7 +565,7 @@ let find_constructor ref f aliases pats scopes =
let v = Environ.constant_value (Global.env()) cst in
unf (global_of_constr v)
| ConstructRef cstr ->
- add_glob loc r;
+ Dumpglob.add_glob loc r;
cstr, [], pats
| _ -> raise Not_found
in unf r
@@ -760,7 +616,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
| CPatNotation (loc, ntn, args) ->
let ntn,args = contract_pat_notation ntn args in
let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
- if !dump then dump_notation_location (patntn_loc loc args ntn) df;
+ if !Flags.dump then Dumpglob.dump_notation_location (Dumpglob.patntn_loc loc args ntn) df;
let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
let ids'',pl = subst_cases_pattern loc (alias_of aliases) intern_pat subst scopes
c
@@ -769,7 +625,7 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope pat =
let a = alias_of aliases in
let (c,df) = Notation.interp_prim_token_cases_pattern loc p a
(tmp_scope,scopes) in
- if !dump then dump_notation_location (fst (unloc loc)) df;
+ if !Flags.dump then Dumpglob.dump_notation_location (fst (unloc loc)) df;
(ids,[subst,c])
| CPatDelimiters (loc, key, e) ->
intern_pat (find_delimiters_scope loc key::scopes) aliases None e
@@ -829,7 +685,7 @@ let push_loc_name_env lvar (ids,tmpsc,scopes as env) loc = function
| Anonymous -> env
| Name id ->
check_hidden_implicit_parameters id lvar;
- dump_binding loc id;
+ Dumpglob.dump_binding loc id;
(Idset.add id ids,tmpsc,scopes)
let intern_typeclass_binders intern_type lvar env bl =
@@ -1029,7 +885,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
intern_notation intern env loc ntn args
| CPrim (loc, p) ->
let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in
- if !dump then dump_notation_location (fst (unloc loc)) df;
+ if !Flags.dump then Dumpglob.dump_notation_location (fst (unloc loc)) df;
c
| CDelimiters (loc, key, e) ->
intern (ids,None,find_delimiters_scope loc key::scopes) e
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index d3b8da8f9..27a46daf1 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -144,10 +144,3 @@ val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
(* Globalization leak for Grammar *)
val for_grammar : ('a -> 'b) -> 'a -> 'b
-
-(* Coqdoc utility functions *)
-type coqdoc_state
-val coqdoc_freeze : unit -> coqdoc_state
-val coqdoc_unfreeze : coqdoc_state -> unit
-
-val add_glob : Util.loc -> global_reference -> unit
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
new file mode 100644
index 000000000..8cc6371f5
--- /dev/null
+++ b/interp/dumpglob.ml
@@ -0,0 +1,220 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id$ *)
+
+
+let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: drop_last tl
+
+(* Dump of globalization (to be used by coqdoc) *)
+
+let glob_file = ref Pervasives.stdout
+
+let open_glob_file f =
+ glob_file := Pervasives.open_out(f ^ ".glob")
+
+let close_glob_file () =
+ Pervasives.close_out !glob_file
+
+let dump_string s =
+ Pervasives.output_string !glob_file s
+
+
+
+(**********************************************************************)
+(* Dump of globalization (to be used by coqdoc) *)
+let token_number = ref 0
+let last_pos = ref 0
+
+type coqdoc_state = Lexer.location_table * int * int
+
+let coqdoc_freeze () =
+ let lt = Lexer.location_table() in
+ let state = (lt,!token_number,!last_pos) in
+ token_number := 0;
+ last_pos := 0;
+ state
+
+let coqdoc_unfreeze (lt,tn,lp) =
+ Lexer.restore_location_table lt;
+ token_number := tn;
+ last_pos := lp
+
+open Decl_kinds
+
+let type_of_logical_kind = function
+ | IsDefinition def ->
+ (match def with
+ | Definition -> "def"
+ | Coercion -> "coe"
+ | SubClass -> "subclass"
+ | CanonicalStructure -> "canonstruc"
+ | Example -> "ex"
+ | Fixpoint -> "def"
+ | CoFixpoint -> "def"
+ | Scheme -> "scheme"
+ | StructureComponent -> "proj"
+ | IdentityCoercion -> "coe"
+ | Instance -> "inst"
+ | Method -> "meth")
+ | IsAssumption a ->
+ (match a with
+ | Definitional -> "defax"
+ | Logical -> "prfax"
+ | Conjectural -> "prfax")
+ | IsProof th ->
+ (match th with
+ | Theorem
+ | Lemma
+ | Fact
+ | Remark
+ | Property
+ | Proposition
+ | Corollary -> "thm")
+
+let type_of_global_ref gr =
+ if Typeclasses.is_class gr then
+ "class"
+ else
+ match gr with
+ | Libnames.ConstRef cst ->
+ type_of_logical_kind (Decls.constant_kind cst)
+ | Libnames.VarRef v ->
+ "var" ^ type_of_logical_kind (Decls.variable_kind v)
+ | Libnames.IndRef ind ->
+ let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
+ if mib.Declarations.mind_record then
+ if mib.Declarations.mind_finite then "rec"
+ else "corec"
+ else if mib.Declarations.mind_finite then "ind"
+ else "coind"
+ | Libnames.ConstructRef _ -> "constr"
+
+let remove_sections dir =
+ if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then
+ (* Not yet (fully) discharged *)
+ Libnames.extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ())
+ else
+ (* Theorem/Lemma outside its outer section of definition *)
+ dir
+
+let dump_ref loc filepath modpath ident ty =
+ dump_string (Printf.sprintf "R%d %s %s %s %s\n"
+ (fst (Util.unloc loc)) filepath modpath ident ty)
+
+let add_glob_gen loc sp lib_dp ty =
+ let mod_dp,id = Libnames.repr_path sp in
+ let mod_dp = remove_sections mod_dp in
+ let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in
+ let filepath = Names.string_of_dirpath lib_dp in
+ let modpath = Names.string_of_dirpath mod_dp_trunc in
+ let ident = Names.string_of_id id in
+ dump_ref loc filepath modpath ident ty
+
+let add_glob loc ref =
+ let sp = Nametab.sp_of_global ref in
+ let lib_dp = Lib.library_part ref in
+ let ty = type_of_global_ref ref in
+ add_glob_gen loc sp lib_dp ty
+
+let add_glob loc ref =
+ if !Flags.dump && loc <> Util.dummy_loc then add_glob loc ref
+
+let mp_of_kn kn =
+ let mp,sec,l = Names.repr_kn kn in
+ Names.MPdot (mp,l)
+
+let add_glob_kn loc kn =
+ let sp = Nametab.sp_of_syntactic_definition kn in
+ let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
+ add_glob_gen loc sp lib_dp "syndef"
+
+let add_glob_kn loc ref =
+ if !Flags.dump && loc <> Util.dummy_loc then add_glob_kn loc ref
+
+let add_local loc id = ()
+(* let mod_dp,id = repr_path sp in *)
+(* let mod_dp = remove_sections mod_dp in *)
+(* let mod_dp_trunc = drop_dirpath_prefix lib_dp mod_dp in *)
+(* let filepath = string_of_dirpath lib_dp in *)
+(* let modpath = string_of_dirpath mod_dp_trunc in *)
+(* let ident = string_of_id id in *)
+(* dump_string (Printf.sprintf "R%d %s %s %s %s\n" *)
+(* (fst (unloc loc)) filepath modpath ident ty) *)
+
+let dump_binding loc id = ()
+
+(* BEGIN obsolete *)
+
+let dump_modref qid = Pp.warning ("Dumpglob.modref: not yet implemented")
+
+let dump_def loc ref =
+ let curr_mp, _ = Lib.current_prefix() in
+ let lib_dp, curr_dp = Lib.split_mp curr_mp in
+ let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp curr_dp in
+
+ let fullname = Libnames.string_of_qualid (Libnames.make_qualid mod_dp_trunc ref) in
+ let filepath = Names.string_of_dirpath lib_dp in
+ dump_string (Printf.sprintf "D%d %s %s\n" (fst (Util.unloc loc)) filepath fullname)
+
+(* END obsolete *)
+
+let dump_definition (loc, id) sec s =
+ dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc))
+ (Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.string_of_id id))
+
+let dump_reference loc modpath ident ty =
+ dump_string (Printf.sprintf "R%d %s %s %s %s\n"
+ (fst (Util.unloc loc)) (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)
+
+let dump_constraint ((loc, n), _, _) sec ty =
+ match n with
+ | Names.Name id -> dump_definition (loc, id) sec ty
+ | Names.Anonymous -> ()
+
+let dump_modref loc mp ty =
+ if !Flags.dump then
+ let (dp, l) = Lib.split_modpath mp in
+ let fp = Names.string_of_dirpath dp in
+ let mp = Names.string_of_dirpath (Names.make_dirpath (drop_last l)) in
+ dump_string (Printf.sprintf "R%d %s %s %s %s\n"
+ (fst (Util.unloc loc)) fp mp "<>" ty)
+
+let dump_moddef loc mp ty =
+ if !Flags.dump then
+ let (dp, l) = Lib.split_modpath mp in
+ let mp = Names.string_of_dirpath (Names.make_dirpath l) in
+ dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp)
+
+let dump_libref loc dp ty =
+ if !Flags.dump then
+ dump_string (Printf.sprintf "R%d %s <> <> %s\n"
+ (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
+
+let loc_of_notation f loc args ntn =
+ if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc)
+ else snd (Util.unloc (f (List.hd args)))
+
+let ntn_loc = loc_of_notation Topconstr.constr_loc
+let patntn_loc = loc_of_notation Topconstr.cases_pattern_expr_loc
+
+let dump_notation_location pos ((path,df),sc) =
+ let rec next growing =
+ let loc = Lexer.location_function !token_number in
+ let (bp,_) = Util.unloc loc in
+ if growing then if bp >= pos then loc else (incr token_number; next true)
+ else if bp = pos then loc
+ else if bp > pos then (decr token_number;next false)
+ else (incr token_number;next true) in
+ let loc = next (pos >= !last_pos) in
+ last_pos := pos;
+ let path = Names.string_of_dirpath path in
+ let _sc = match sc with Some sc -> " "^sc | None -> "" in
+ dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (Util.unloc loc)) path df)
+
+
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 0af11bad9..3482dd3a0 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -61,34 +61,6 @@ let lookup_qualid (modtype:bool) qid =
*)
-let split_modpath mp =
- let rec aux = function
- | MPfile dp -> dp, []
- | MPbound mbid ->
- Lib.library_dp (), [id_of_mbid mbid]
- | MPself msid -> Lib.library_dp (), [id_of_msid msid]
- | MPdot (mp,l) -> let (mp', lab) = aux mp in
- (mp', id_of_label l :: lab)
- in
- let (mp, l) = aux mp in
- mp, l
-
-let dump_moddef loc mp ty =
- if !Flags.dump then
- let (dp, l) = split_modpath mp in
- let mp = string_of_dirpath (make_dirpath l) in
- Flags.dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (unloc loc)) "<>" mp)
-
-let rec drop_last = function [] -> assert false | hd :: [] -> [] | hd :: tl -> hd :: drop_last tl
-
-let dump_modref loc mp ty =
- if !Flags.dump then
- let (dp, l) = split_modpath mp in
- let fp = string_of_dirpath dp in
- let mp = string_of_dirpath (make_dirpath (drop_last l)) in
- Flags.dump_string (Printf.sprintf "R%d %s %s %s %s\n"
- (fst (unloc loc)) fp mp "<>" ty)
-
(* Search for the head of [qid] in [binders].
If found, returns the module_path/kernel_name created from the dirpath
and the basename. Searches Nametab otherwise.
@@ -96,14 +68,14 @@ let dump_modref loc mp ty =
let lookup_module (loc,qid) =
try
let mp = Nametab.locate_module qid in
- dump_modref loc mp "modtype"; mp
+ Dumpglob.dump_modref loc mp "modtype"; mp
with
| Not_found -> Modops.error_not_a_module_loc loc (string_of_qualid qid)
let lookup_modtype (loc,qid) =
try
let mp = Nametab.locate_modtype qid in
- dump_modref loc mp "mod"; mp
+ Dumpglob.dump_modref loc mp "mod"; mp
with
| Not_found ->
Modops.error_not_a_modtype_loc loc (string_of_qualid qid)
diff --git a/interp/modintern.mli b/interp/modintern.mli
index c14b6481e..1f27e3c18 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -26,6 +26,3 @@ val interp_modtype : env -> module_type_ast -> module_struct_entry
val interp_modexpr : env -> module_ast -> module_struct_entry
val lookup_module : qualid located -> module_path
-
-val dump_moddef : loc -> module_path -> string -> unit
-val dump_modref : loc -> module_path -> string -> unit
diff --git a/kernel/names.ml b/kernel/names.ml
index 975390cb9..3d80ad23e 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -86,6 +86,7 @@ type label = string
type mod_self_id = uniq_ident
let make_msid = make_uid
+let repr_msid (n, id, dp) = (n, id, dp)
let debug_string_of_msid = debug_string_of_uid
let refresh_msid (_,s,dir) = make_uid dir s
let string_of_msid = string_of_uid
@@ -94,6 +95,7 @@ let label_of_msid (_,s,_) = s
type mod_bound_id = uniq_ident
let make_mbid = make_uid
+let repr_mbid (n, id, dp) = (n, id, dp)
let debug_string_of_mbid = debug_string_of_uid
let string_of_mbid = string_of_uid
let id_of_mbid (_,s,_) = s
@@ -116,7 +118,7 @@ type module_path =
| MPdot of module_path * label
let rec string_of_mp = function
- | MPfile sl -> string_of_dirpath sl
+ | MPfile sl -> "MPfile (" ^ string_of_dirpath sl ^ ")"
| MPbound uid -> string_of_uid uid
| MPself uid -> string_of_uid uid
| MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
diff --git a/kernel/names.mli b/kernel/names.mli
index b19f93e2d..177768cf4 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -48,6 +48,7 @@ type mod_self_id
(* The first argument is a file name - to prevent conflict between
different files *)
val make_msid : dir_path -> string -> mod_self_id
+val repr_msid : mod_self_id -> int * string * dir_path
val id_of_msid : mod_self_id -> identifier
val label_of_msid : mod_self_id -> label
val refresh_msid : mod_self_id -> mod_self_id
@@ -58,6 +59,7 @@ val string_of_msid : mod_self_id -> string
type mod_bound_id
val make_mbid : dir_path -> string -> mod_bound_id
+val repr_mbid : mod_bound_id -> int * string * dir_path
val id_of_mbid : mod_bound_id -> identifier
val label_of_mbid : mod_bound_id -> label
val debug_string_of_mbid : mod_bound_id -> string
@@ -82,7 +84,6 @@ type module_path =
| MPdot of module_path * label
(*i | MPapply of module_path * module_path in the future (maybe) i*)
-
val string_of_mp : module_path -> string
module MPset : Set.S with type elt = module_path
diff --git a/lib/flags.ml b/lib/flags.ml
index 68e287f69..f2ab87b4b 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -86,23 +86,6 @@ let is_unsafe s = Stringset.mem s !unsafe_set
let noglob = ref false
let dump = ref false
-let dump_file = ref ""
-let dump_into_file f = dump := true; dump_file := f
-
-let dump_buffer = Buffer.create 8192
-
-let dump_string = Buffer.add_string dump_buffer
-
-let dump_it () =
- if !dump then begin
- let mode = [Open_wronly; Open_creat] in
- let c = open_out_gen mode 0o666 !dump_file in
- output_string c (Buffer.contents dump_buffer);
- Buffer.clear dump_buffer;
- close_out c
- end
-
-let _ = at_exit dump_it
(* Flags.for the virtual machine *)
diff --git a/lib/flags.mli b/lib/flags.mli
index 08f9a279d..4cab30381 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -61,9 +61,6 @@ val is_unsafe : string -> bool
val noglob : bool ref
val dump : bool ref
-val dump_into_file : string -> unit
-val dump_string : string -> unit
-val dump_it : unit -> unit
(* Options for the virtual machine *)
diff --git a/library/lib.ml b/library/lib.ml
index 5e22c4d22..bb0ad74ca 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -10,7 +10,6 @@
open Pp
open Util
-open Names
open Libnames
open Nameops
open Libobject
@@ -33,7 +32,7 @@ and library_entry = object_name * node
and library_segment = library_entry list
-type lib_objects = (identifier * obj) list
+type lib_objects = (Names.identifier * obj) list
let iter_objects f i prefix =
List.iter (fun (id,obj) -> f i (make_oname prefix id, obj))
@@ -53,7 +52,7 @@ let classify_segment seg =
let rec clean ((substl,keepl,anticipl) as acc) = function
| (_,CompilingLibrary _) :: _ | [] -> acc
| ((sp,kn as oname),Leaf o) :: stk ->
- let id = id_of_label (label kn) in
+ let id = Names.id_of_label (Names.label kn) in
(match classify_object (oname,o) with
| Dispose -> clean acc stk
| Keep o' ->
@@ -85,7 +84,7 @@ let segment_of_objects prefix =
sections, but on the contrary there are many constructions of section
paths based on the library path. *)
-let initial_prefix = default_library,(initial_path,empty_dirpath)
+let initial_prefix = default_library,(Names.initial_path,Names.empty_dirpath)
let lib_stk = ref ([] : library_segment)
@@ -98,8 +97,21 @@ let library_dp () =
module path and relative section path *)
let path_prefix = ref initial_prefix
+let sections_depth () =
+ List.length (Names.repr_dirpath (snd (snd !path_prefix)))
+
+let sections_are_opened () =
+ match Names.repr_dirpath (snd (snd !path_prefix)) with
+ [] -> false
+ | _ -> true
+
let cwd () = fst !path_prefix
+let current_dirpath sec =
+ Libnames.drop_dirpath_prefix (library_dp ())
+ (if sec then cwd ()
+ else Libnames.extract_dirpath_prefix (sections_depth ()) (cwd ()))
+
let make_path id = Libnames.make_path (cwd ()) id
let path_of_include () =
@@ -112,25 +124,15 @@ let current_prefix () = snd !path_prefix
let make_kn id =
let mp,dir = current_prefix () in
- Names.make_kn mp dir (label_of_id id)
+ Names.make_kn mp dir (Names.label_of_id id)
let make_con id =
let mp,dir = current_prefix () in
- Names.make_con mp dir (label_of_id id)
+ Names.make_con mp dir (Names.label_of_id id)
let make_oname id = make_path id, make_kn id
-
-let sections_depth () =
- List.length (repr_dirpath (snd (snd !path_prefix)))
-
-let sections_are_opened () =
- match repr_dirpath (snd (snd !path_prefix)) with
- [] -> false
- | _ -> true
-
-
let recalc_path_prefix () =
let rec recalc = function
| (sp, OpenedSection (dir,_)) :: _ -> dir
@@ -194,7 +196,7 @@ let add_entry sp node =
let anonymous_id =
let n = ref 0 in
- fun () -> incr n; id_of_string ("_" ^ (string_of_int !n))
+ fun () -> incr n; Names.id_of_string ("_" ^ (string_of_int !n))
let add_anonymous_entry node =
let id = anonymous_id () in
@@ -207,7 +209,7 @@ let add_absolutely_named_leaf sp obj =
add_entry sp (Leaf obj)
let add_leaf id obj =
- if fst (current_prefix ()) = initial_path then
+ if fst (current_prefix ()) = Names.initial_path then
error ("No session module started (use -top dir)");
let oname = make_oname id in
cache_object (oname,obj);
@@ -261,7 +263,7 @@ let current_mod_id () =
let start_module export id mp nametab =
let dir = extend_dirpath (fst !path_prefix) id in
- let prefix = dir,(mp,empty_dirpath) in
+ let prefix = dir,(mp,Names.empty_dirpath) in
let oname = make_path id, make_kn id in
if Nametab.exists_module dir then
errorlabstrm "open_module" (pr_id id ++ str " already exists") ;
@@ -306,7 +308,7 @@ let end_module id =
let start_modtype id mp nametab =
let dir = extend_dirpath (fst !path_prefix) id in
- let prefix = dir,(mp,empty_dirpath) in
+ let prefix = dir,(mp,Names.empty_dirpath) in
let sp = make_path id in
let name = sp, make_kn id in
if Nametab.exists_cci sp then
@@ -363,9 +365,9 @@ let check_for_comp_unit () =
let start_compilation s mp =
if !comp_name <> None then
error "compilation unit is already started";
- if snd (snd (!path_prefix)) <> empty_dirpath then
+ if snd (snd (!path_prefix)) <> Names.empty_dirpath then
error "some sections are already opened";
- let prefix = s, (mp, empty_dirpath) in
+ let prefix = s, (mp, Names.empty_dirpath) in
let _ = add_anonymous_entry (CompilingLibrary prefix) in
comp_name := Some s;
path_prefix := prefix
@@ -395,8 +397,8 @@ let end_compilation dir =
| None -> anomaly "There should be a module name..."
| Some m ->
if m <> dir then anomaly
- ("The current open module has name "^ (string_of_dirpath m) ^
- " and not " ^ (string_of_dirpath m));
+ ("The current open module has name "^ (Names.string_of_dirpath m) ^
+ " and not " ^ (Names.string_of_dirpath m));
in
let (after,_,before) = split_lib oname in
comp_name := None;
@@ -437,13 +439,13 @@ let what_is_opened () = find_entry_p is_something_opened
- the list of substitution to do at section closing
*)
-type abstr_list = Sign.named_context Cmap.t * Sign.named_context KNmap.t
+type abstr_list = Sign.named_context Names.Cmap.t * Sign.named_context Names.KNmap.t
let sectab =
- ref ([] : ((identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list)
+ ref ([] : ((Names.identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list)
let add_section () =
- sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab
+ sectab := ([],(Names.Cmap.empty,Names.KNmap.empty),(Names.Cmap.empty,Names.KNmap.empty)) :: !sectab
let add_section_variable id impl keep =
match !sectab with
@@ -465,11 +467,11 @@ let add_section_replacement f g hyps =
sectab := (vars,f (Array.map Term.destVar args) exps,g sechyps abs)::sl
let add_section_kn kn =
- let f = (fun x (l1,l2) -> (l1,KNmap.add kn x l2)) in
+ let f = (fun x (l1,l2) -> (l1,Names.KNmap.add kn x l2)) in
add_section_replacement f f
let add_section_constant kn =
- let f = (fun x (l1,l2) -> (Cmap.add kn x l1,l2)) in
+ let f = (fun x (l1,l2) -> (Names.Cmap.add kn x l1,l2)) in
add_section_replacement f f
let replacement_context () = pi2 (List.hd !sectab)
@@ -477,17 +479,17 @@ let replacement_context () = pi2 (List.hd !sectab)
let variables_context () = pi1 (List.hd !sectab)
let section_segment_of_constant con =
- Cmap.find con (fst (pi3 (List.hd !sectab)))
+ Names.Cmap.find con (fst (pi3 (List.hd !sectab)))
let section_segment_of_mutual_inductive kn =
- KNmap.find kn (snd (pi3 (List.hd !sectab)))
+ Names.KNmap.find kn (snd (pi3 (List.hd !sectab)))
let section_instance = function
| VarRef id -> [||]
| ConstRef con ->
- Cmap.find con (fst (pi2 (List.hd !sectab)))
+ Names.Cmap.find con (fst (pi2 (List.hd !sectab)))
| IndRef (kn,_) | ConstructRef ((kn,_),_) ->
- KNmap.find kn (snd (pi2 (List.hd !sectab)))
+ Names.KNmap.find kn (snd (pi2 (List.hd !sectab)))
let init_sectab () = sectab := []
let freeze_sectab () = !sectab
@@ -713,7 +715,7 @@ let back n = reset_to (back_stk n !lib_stk)
(* State and initialization. *)
-type frozen = dir_path option * library_segment
+type frozen = Names.dir_path option * library_segment
let freeze () = (!comp_name, !lib_stk)
@@ -757,16 +759,37 @@ let reset_initial () =
let mp_of_global ref =
match ref with
| VarRef id -> fst (current_prefix ())
- | ConstRef cst -> con_modpath cst
- | IndRef ind -> ind_modpath ind
- | ConstructRef constr -> constr_modpath constr
+ | ConstRef cst -> Names.con_modpath cst
+ | IndRef ind -> Names.ind_modpath ind
+ | ConstructRef constr -> Names.constr_modpath constr
let rec dp_of_mp modp =
match modp with
- | MPfile dp -> dp
- | MPbound _ | MPself _ -> library_dp ()
- | MPdot (mp,_) -> dp_of_mp mp
-
+ | Names.MPfile dp -> dp
+ | Names.MPbound _ | Names.MPself _ -> library_dp ()
+ | Names.MPdot (mp,_) -> dp_of_mp mp
+
+let rec split_mp mp =
+ match mp with
+ | Names.MPfile dp -> dp, Names.empty_dirpath
+ | Names.MPdot (prfx, lbl) ->
+ let mprec, dprec = split_mp prfx in
+ mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec))
+ | Names.MPself msid -> let (_, id, dp) = Names.repr_msid msid in library_dp(), Names.make_dirpath [Names.id_of_string id]
+ | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.make_dirpath [Names.id_of_string id]
+
+let split_modpath mp =
+ let rec aux = function
+ | Names.MPfile dp -> dp, []
+ | Names.MPbound mbid ->
+ library_dp (), [Names.id_of_mbid mbid]
+ | Names.MPself msid -> library_dp (), [Names.id_of_msid msid]
+ | Names.MPdot (mp,l) -> let (mp', lab) = aux mp in
+ (mp', Names.id_of_label l :: lab)
+ in
+ let (mp, l) = aux mp in
+ mp, l
+
let library_part ref =
match ref with
| VarRef id -> library_dp ()
@@ -798,12 +821,12 @@ let pop_con con =
Names.make_con mp (dirpath_prefix dir) l
let con_defined_in_sec kn =
- let _,dir,_ = repr_con kn in
- dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+ let _,dir,_ = Names.repr_con kn in
+ dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
let defined_in_sec kn =
- let _,dir,_ = repr_kn kn in
- dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
+ let _,dir,_ = Names.repr_kn kn in
+ dir <> Names.empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ())
let discharge_global = function
| ConstRef kn when con_defined_in_sec kn ->
diff --git a/library/lib.mli b/library/lib.mli
index 03498f5d9..80ce26fc6 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -8,39 +8,31 @@
(*i $Id$ i*)
-(*i*)
-open Util
-open Names
-open Libnames
-open Libobject
-open Summary
-open Mod_subst
-(*i*)
(*s This module provides a general mechanism to keep a trace of all operations
and to backtrack (undo) those operations. It provides also the section
mechanism (at a low level; discharge is not known at this step). *)
type node =
- | Leaf of obj
- | CompilingLibrary of object_prefix
- | OpenedModule of bool option * object_prefix * Summary.frozen
+ | Leaf of Libobject.obj
+ | CompilingLibrary of Libnames.object_prefix
+ | OpenedModule of bool option * Libnames.object_prefix * Summary.frozen
| ClosedModule of library_segment
- | OpenedModtype of object_prefix * Summary.frozen
+ | OpenedModtype of Libnames.object_prefix * Summary.frozen
| ClosedModtype of library_segment
- | OpenedSection of object_prefix * Summary.frozen
+ | OpenedSection of Libnames.object_prefix * Summary.frozen
| ClosedSection of library_segment
| FrozenState of Summary.frozen
-and library_segment = (object_name * node) list
+and library_segment = (Libnames.object_name * node) list
-type lib_objects = (identifier * obj) list
+type lib_objects = (Names.identifier * Libobject.obj) list
(*s Object iteratation functions. *)
-val open_objects : int -> object_prefix -> lib_objects -> unit
-val load_objects : int -> object_prefix -> lib_objects -> unit
-val subst_objects : object_prefix -> substitution -> lib_objects -> lib_objects
+val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit
+val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit
+val subst_objects : Libnames.object_prefix -> Mod_subst.substitution -> lib_objects -> lib_objects
(* [classify_segment seg] verifies that there are no OpenedThings,
clears ClosedSections and FrozenStates and divides Leafs according
@@ -48,23 +40,23 @@ val subst_objects : object_prefix -> substitution -> lib_objects -> lib_objects
[Substitute], [Keep], [Anticipate] respectively. The order of each
returned list is the same as in the input list. *)
val classify_segment :
- library_segment -> lib_objects * lib_objects * obj list
+ library_segment -> lib_objects * lib_objects * Libobject.obj list
(* [segment_of_objects prefix objs] forms a list of Leafs *)
val segment_of_objects :
- object_prefix -> lib_objects -> library_segment
+ Libnames.object_prefix -> lib_objects -> library_segment
(*s Adding operations (which call the [cache] method, and getting the
current list of operations (most recent ones coming first). *)
-val add_leaf : identifier -> obj -> object_name
-val add_absolutely_named_leaf : object_name -> obj -> unit
-val add_anonymous_leaf : obj -> unit
+val add_leaf : Names.identifier -> Libobject.obj -> Libnames.object_name
+val add_absolutely_named_leaf : Libnames.object_name -> Libobject.obj -> unit
+val add_anonymous_leaf : Libobject.obj -> unit
(* this operation adds all objects with the same name and calls [load_object]
for each of them *)
-val add_leaves : identifier -> obj list -> object_name
+val add_leaves : Names.identifier -> Libobject.obj list -> Libnames.object_name
val add_frozen_state : unit -> unit
@@ -81,19 +73,20 @@ val reset_label : int -> unit
starting from a given section path. If not given, the entire segment
is returned. *)
-val contents_after : object_name option -> library_segment
+val contents_after : Libnames.object_name option -> library_segment
(*s Functions relative to current path *)
(* User-side names *)
-val cwd : unit -> dir_path
-val make_path : identifier -> section_path
-val path_of_include : unit -> section_path
+val cwd : unit -> Names.dir_path
+val current_dirpath : bool -> Names.dir_path
+val make_path : Names.identifier -> Libnames.section_path
+val path_of_include : unit -> Libnames.section_path
(* Kernel-side names *)
-val current_prefix : unit -> module_path * dir_path
-val make_kn : identifier -> kernel_name
-val make_con : identifier -> constant
+val current_prefix : unit -> Names.module_path * Names.dir_path
+val make_kn : Names.identifier -> Names.kernel_name
+val make_con : Names.identifier -> Names.constant
(* Are we inside an opened section *)
val sections_are_opened : unit -> bool
@@ -102,53 +95,55 @@ val sections_depth : unit -> int
(* Are we inside an opened module type *)
val is_modtype : unit -> bool
val is_module : unit -> bool
-val current_mod_id : unit -> module_ident
+val current_mod_id : unit -> Names.module_ident
(* Returns the most recent OpenedThing node *)
-val what_is_opened : unit -> object_name * node
+val what_is_opened : unit -> Libnames.object_name * node
(*s Modules and module types *)
val start_module :
- bool option -> module_ident -> module_path -> Summary.frozen -> object_prefix
-val end_module : module_ident
- -> object_name * object_prefix * Summary.frozen * library_segment
+ bool option -> Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix
+val end_module : Names.module_ident
+ -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment
val start_modtype :
- module_ident -> module_path -> Summary.frozen -> object_prefix
-val end_modtype : module_ident
- -> object_name * object_prefix * Summary.frozen * library_segment
+ Names.module_ident -> Names.module_path -> Summary.frozen -> Libnames.object_prefix
+val end_modtype : Names.module_ident
+ -> Libnames.object_name * Libnames.object_prefix * Summary.frozen * library_segment
(* [Lib.add_frozen_state] must be called after each of the above functions *)
(*s Compilation units *)
-val start_compilation : dir_path -> module_path -> unit
-val end_compilation : dir_path -> object_prefix * library_segment
+val start_compilation : Names.dir_path -> Names.module_path -> unit
+val end_compilation : Names.dir_path -> Libnames.object_prefix * library_segment
(* The function [library_dp] returns the [dir_path] of the current
compiling library (or [default_library]) *)
-val library_dp : unit -> dir_path
+val library_dp : unit -> Names.dir_path
(* Extract the library part of a name even if in a section *)
-val dp_of_mp : module_path -> dir_path
-val library_part : global_reference -> dir_path
-val remove_section_part : global_reference -> dir_path
+val dp_of_mp : Names.module_path -> Names.dir_path
+val split_mp : Names.module_path -> Names.dir_path * Names.dir_path
+val split_modpath : Names.module_path -> Names.dir_path * Names.identifier list
+val library_part : Libnames.global_reference -> Names.dir_path
+val remove_section_part : Libnames.global_reference -> Names.dir_path
(*s Sections *)
-val open_section : identifier -> unit
-val close_section : identifier -> unit
+val open_section : Names.identifier -> unit
+val close_section : Names.identifier -> unit
(*s Backtracking (undo). *)
-val reset_to : object_name -> unit
-val reset_name : identifier located -> unit
-val remove_name : identifier located -> unit
-val reset_mod : identifier located -> unit
-val reset_to_state : object_name -> unit
+val reset_to : Libnames.object_name -> unit
+val reset_name : Names.identifier Util.located -> unit
+val remove_name : Names.identifier Util.located -> unit
+val reset_mod : Names.identifier Util.located -> unit
+val reset_to_state : Libnames.object_name -> unit
-val has_top_frozen_state : unit -> object_name option
+val has_top_frozen_state : unit -> Libnames.object_name option
(* [back n] resets to the place corresponding to the $n$-th call of
[mark_end_of_command] (counting backwards) *)
@@ -168,28 +163,28 @@ val reset_initial : unit -> unit
(* XML output hooks *)
-val set_xml_open_section : (identifier -> unit) -> unit
-val set_xml_close_section : (identifier -> unit) -> unit
+val set_xml_open_section : (Names.identifier -> unit) -> unit
+val set_xml_close_section : (Names.identifier -> unit) -> unit
(*s Section management for discharge *)
-val section_segment_of_constant : constant -> Sign.named_context
-val section_segment_of_mutual_inductive: mutual_inductive -> Sign.named_context
+val section_segment_of_constant : Names.constant -> Sign.named_context
+val section_segment_of_mutual_inductive: Names.mutual_inductive -> Sign.named_context
-val section_instance : global_reference -> identifier array
+val section_instance : Libnames.global_reference -> Names.identifier array
-val add_section_variable : identifier -> bool -> Term.types option -> unit
-val add_section_constant : constant -> Sign.named_context -> unit
-val add_section_kn : kernel_name -> Sign.named_context -> unit
+val add_section_variable : Names.identifier -> bool -> Term.types option -> unit
+val add_section_constant : Names.constant -> Sign.named_context -> unit
+val add_section_kn : Names.kernel_name -> Sign.named_context -> unit
val replacement_context : unit ->
- (identifier array Cmap.t * identifier array KNmap.t)
+ (Names.identifier array Names.Cmap.t * Names.identifier array Names.KNmap.t)
(*s Discharge: decrease the section level if in the current section *)
-val discharge_kn : kernel_name -> kernel_name
-val discharge_con : constant -> constant
-val discharge_global : global_reference -> global_reference
-val discharge_inductive : inductive -> inductive
+val discharge_kn : Names.kernel_name -> Names.kernel_name
+val discharge_con : Names.constant -> Names.constant
+val discharge_global : Libnames.global_reference -> Libnames.global_reference
+val discharge_inductive : Names.inductive -> Names.inductive
diff --git a/library/library.ml b/library/library.ml
index 2f74fe92b..272f01f7d 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -18,7 +18,6 @@ open Safe_typing
open Libobject
open Lib
open Nametab
-open Declaremods
(*************************************************************************)
(*s Load path. Mapping from physical to logical paths etc.*)
@@ -113,7 +112,7 @@ type compilation_unit_name = dir_path
type library_disk = {
md_name : compilation_unit_name;
md_compiled : compiled_library;
- md_objects : library_objects;
+ md_objects : Declaremods.library_objects;
md_deps : (compilation_unit_name * Digest.t) list;
md_imports : compilation_unit_name list }
@@ -123,7 +122,7 @@ type library_disk = {
type library_t = {
library_name : compilation_unit_name;
library_compiled : compiled_library;
- library_objects : library_objects;
+ library_objects : Declaremods.library_objects;
library_deps : (compilation_unit_name * Digest.t) list;
library_imports : compilation_unit_name list;
library_digest : Digest.t }
@@ -540,19 +539,16 @@ let require_library qidl export =
let modrefl = List.map try_locate_qualified_library qidl in
let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in
let modrefl = List.map fst modrefl in
- if Lib.is_modtype () || Lib.is_module () then begin
- add_anonymous_leaf (in_require (needed,modrefl,None));
- Option.iter (fun exp ->
- List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl)
- export
- end
+ if Lib.is_modtype () || Lib.is_module () then
+ begin
+ add_anonymous_leaf (in_require (needed,modrefl,None));
+ Option.iter (fun exp ->
+ List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl)
+ export
+ end
else
add_anonymous_leaf (in_require (needed,modrefl,export));
- if !Flags.dump then List.iter2 (fun (loc, _) dp ->
- Flags.dump_string (Printf.sprintf "R%d %s <> <> %s\n"
- (fst (unloc loc)) (string_of_dirpath dp) "lib"))
- qidl modrefl;
- if !Flags.xml_export then List.iter !xml_require modrefl;
+ if !Flags.xml_export then List.iter !xml_require modrefl;
add_frozen_state ()
let require_library_from_file idopt file export =
@@ -573,18 +569,18 @@ let require_library_from_file idopt file export =
let import_module export (loc,qid) =
try
match Nametab.locate_module qid with
- MPfile dir ->
+ | MPfile dir ->
if Lib.is_modtype () || Lib.is_module () || not export then
add_anonymous_leaf (in_import (dir, export))
else
add_anonymous_leaf (in_require ([],[dir], Some export))
| mp ->
- import_module export mp
+ Declaremods.import_module export mp
with
Not_found ->
user_err_loc
- (loc,"import_library",
- str ((string_of_qualid qid)^" is not a module"))
+ (loc,"import_library",
+ str ((string_of_qualid qid)^" is not a module"))
(************************************************************************)
(*s Initializing the compilation of a library. *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index a4933a896..0d5d27538 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -441,7 +441,7 @@ let add_hints local dbnames0 h =
(str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++
str "to an evaluable reference")
in
- if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr;
+ if !Flags.dump then Dumpglob.add_glob (loc_of_reference r) gr;
(gr,r') in
add_unfolds (List.map f lhints) local dbnames
| HintsConstructors lqid ->
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index ab23f2210..e4d464236 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -238,7 +238,9 @@ let firstchar =
let identchar =
['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255'
'\'' '0'-'9']
-let ident = firstchar identchar*
+let id = firstchar identchar*
+let pfx_id = (id '.')*
+let ident = id | pfx_id id
let begin_hide = "(*" space* "begin" space+ "hide" space* "*)"
let end_hide = "(*" space* "end" space+ "hide" space* "*)"
@@ -405,10 +407,11 @@ and module_refs = parse
{ module_refs lexbuf }
| ident
{ let id = lexeme lexbuf in
- (try
- add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id
- with
- Not_found -> ()
+ (Printf.eprintf "DEBUG: id = %s\n" id;
+ try
+ add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id
+ with
+ Not_found -> ()
);
module_refs lexbuf }
| eof
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 0522bbac0..a75b7196d 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -417,17 +417,14 @@ module Html = struct
let stop_verbatim () = printf "</pre>\n"
let module_ref m s =
- printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
- (*i
match find_module m with
- | Local ->
- printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
- | Coqlib when !externals ->
- let m = Filename.concat !coqlib m in
- printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
- | Coqlib | Unknown ->
- raw_ident s
- i*)
+ | Local ->
+ printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
+ | Coqlib when !externals ->
+ let m = Filename.concat !coqlib m in
+ printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
+ | Coqlib | Unknown ->
+ raw_ident s
let ident_ref m fid s =
match find_module m with
@@ -446,6 +443,7 @@ module Html = struct
printf "</span>"
end else
begin
+ Printf.eprintf "DEBUG: looking for (%s, %d)\n" !current_module loc;
try
(match Index.find !current_module loc with
| Def (fullid,_) ->
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index d78aabbf9..b2fa915b6 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -639,7 +639,7 @@ and notation_bol = parse
and notation = parse
| nl { Output.line_break(); notation_bol lexbuf }
- | '"' { Output.char '"'; false }
+ | '"' { Output.char '"'}
| token
{ let s = lexeme lexbuf in
Output.symbol s; notation lexbuf }
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 30fee26a0..d07051b71 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -447,7 +447,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
try
let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
- Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
+ Dumpglob.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
c :: props, rest'
with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
([], props) k.cl_props
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 02044b2cf..83a4703a2 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -108,15 +108,11 @@ let add_compile verbose s =
compile_list := (verbose,s) :: !compile_list
let compile_files () =
let init_state = States.freeze() in
- let coqdoc_init_state = Constrintern.coqdoc_freeze () in
+ let coqdoc_init_state = Dumpglob.coqdoc_freeze () in
List.iter
(fun (v,f) ->
States.unfreeze init_state;
- Constrintern.coqdoc_unfreeze coqdoc_init_state;
- if !Flags.noglob then
- Flags.dump := false
- else
- Flags.dump_into_file (f^".glob");
+ Dumpglob.coqdoc_unfreeze coqdoc_init_state;
if Flags.do_translate () then
with_option translate_file (Vernac.compile v) f
else
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index c0ec55228..d3c556147 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -126,7 +126,7 @@ let rec vernac_com interpfun (loc,com) =
let cl = !Pp.comments in
(* end translator state *)
(* coqdoc state *)
- let cds = Constrintern.coqdoc_freeze() in
+ let cds = Dumpglob.coqdoc_freeze() in
if !Flags.translate_file then
begin
let _,f = find_file_in_path (Library.get_load_paths ())
@@ -141,13 +141,13 @@ let rec vernac_com interpfun (loc,com) =
chan_translate := ch;
Lexer.restore_com_state cs;
Pp.comments := cl;
- Constrintern.coqdoc_unfreeze cds
+ Dumpglob.coqdoc_unfreeze cds
with e ->
if !Flags.translate_file then close_out !chan_translate;
chan_translate := ch;
Lexer.restore_com_state cs;
Pp.comments := cl;
- Constrintern.coqdoc_unfreeze cds;
+ Dumpglob.coqdoc_unfreeze cds;
raise e
end
@@ -228,14 +228,15 @@ let compile verbosely f =
let ldir,long_f_dot_v = Library.start_library f in
let dumpstate = !Flags.dump in
if not !Flags.noglob then
- (Flags.dump_into_file (f ^ ".glob");
- Flags.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"));
+ (Flags.dump := true;
+ Dumpglob.open_glob_file f;
+ Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n"));
if !Flags.xml_export then !xml_start_library ();
let _ = load_vernac verbosely long_f_dot_v in
if Pfedit.get_all_proof_names () <> [] then
(message "Error: There are pending proofs"; exit 1);
if !Flags.xml_export then !xml_end_library ();
- if !Flags.dump then Flags.dump_it ();
+ if !Flags.dump then Dumpglob.close_glob_file ();
Flags.dump := dumpstate;
Library.save_library_to ldir (long_f_dot_v ^ "o")
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2cea826a7..d1003bd83 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -275,7 +275,7 @@ let print_located_module r =
let global_with_alias r =
let gr = global_with_alias r in
- if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr;
+ if !Flags.dump then Dumpglob.add_glob (loc_of_reference r) gr;
gr
(**********)
@@ -305,49 +305,31 @@ let start_proof_and_print k l hook =
print_subgoals ();
if !pcoq <> None then (Option.get !pcoq).start_proof ()
-let current_dirpath sec =
- drop_dirpath_prefix (Lib.library_dp ())
- (if sec then Lib.cwd ()
- else extract_dirpath_prefix (Lib.sections_depth ()) (Lib.cwd ()))
-
-let dump_definition (loc, id) sec s =
- Flags.dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (unloc loc))
- (string_of_dirpath (current_dirpath sec)) (string_of_id id))
-
-let dump_reference loc modpath ident ty =
- dump_string (Printf.sprintf "R%d %s %s %s %s\n"
- (fst (unloc loc)) (string_of_dirpath (Lib.library_dp ())) modpath ident ty)
-
-let dump_constraint ((loc, n), _, _) sec ty =
- match n with
- | Name id -> dump_definition (loc, id) sec ty
- | Anonymous -> ()
-
-let vernac_definition (local,_,_ as k) (_,id as lid) def hook =
- if !Flags.dump then dump_definition lid false "def";
- match def with
- | ProveBody (bl,t) -> (* local binders, typ *)
- if Lib.is_modtype () then
- errorlabstrm "Vernacentries.VernacDefinition"
- (str "Proof editing mode not supported in module types")
- else
- let hook _ _ = () in
- start_proof_and_print (local,DefinitionBody Definition)
- [Some lid,(bl,t)] hook
- | DefineBody (bl,red_option,c,typ_opt) ->
- let red_option = match red_option with
- | None -> None
- | Some r ->
- let (evc,env)= Command.get_current_context () in
- Some (interp_redexp env evc r) in
- declare_definition id k bl red_option c typ_opt hook
-
+let vernac_definition (local,_,_ as k) (loc,id as lid) def hook =
+ if !Flags.dump then Dumpglob.dump_definition lid false "def";
+ (match def with
+ | ProveBody (bl,t) -> (* local binders, typ *)
+ if Lib.is_modtype () then
+ errorlabstrm "Vernacentries.VernacDefinition"
+ (str "Proof editing mode not supported in module types")
+ else
+ let hook _ _ = () in
+ start_proof_and_print (local,DefinitionBody Definition)
+ [Some lid, (bl,t)] hook
+ | DefineBody (bl,red_option,c,typ_opt) ->
+ let red_option = match red_option with
+ | None -> None
+ | Some r ->
+ let (evc,env)= Command.get_current_context () in
+ Some (interp_redexp env evc r) in
+ declare_definition id k bl red_option c typ_opt hook)
+
let vernac_start_proof kind l lettop hook =
if !Flags.dump then
List.iter (fun (id, _) ->
match id with
- | Some lid -> dump_definition lid false "prf"
- | None -> ()) l;
+ | Some lid -> Dumpglob.dump_definition lid false "prf"
+ | None -> ()) l;
if not(refining ()) then
if lettop then
errorlabstrm "Vernacentries.StartProof"
@@ -381,28 +363,28 @@ let vernac_exact_proof c =
let vernac_assumption kind l nl=
let global = fst kind = Global in
- List.iter (fun (is_coe,(idl,c)) ->
- if !dump then
- List.iter (fun lid ->
- if global then dump_definition lid false "ax"
- else dump_definition lid true "var") idl;
- declare_assumption idl is_coe kind [] c false false nl) l
-
+ List.iter (fun (is_coe,(idl,c)) ->
+ if !dump then
+ List.iter (fun lid ->
+ if global then Dumpglob.dump_definition lid false "ax"
+ else Dumpglob.dump_definition lid true "var") idl;
+ declare_assumption idl is_coe kind [] c false false nl) l
+
let vernac_inductive f indl =
if !dump then
List.iter (fun ((lid, _, _, cstrs), _) ->
- dump_definition lid false"ind";
+ Dumpglob.dump_definition lid false"ind";
List.iter (fun (_, (lid, _)) ->
- dump_definition lid false "constr") cstrs)
+ Dumpglob.dump_definition lid false "constr") cstrs)
indl;
build_mutual indl f
let vernac_fixpoint l b =
- List.iter (fun ((lid, _, _, _, _), _) -> dump_definition lid false "def") l;
+ List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
build_recursive l b
let vernac_cofixpoint l b =
- List.iter (fun ((lid, _, _, _), _) -> dump_definition lid false "def") l;
+ List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
build_corecursive l b
let vernac_scheme = build_scheme
@@ -413,9 +395,11 @@ let vernac_combined_scheme = build_combined_scheme
(* Modules *)
let vernac_import export refl =
- let import ref = Library.import_module export (qualid_of_reference ref) in
- List.iter import refl;
- Lib.add_frozen_state ()
+ let import ref =
+ Library.import_module export (qualid_of_reference ref)
+ in
+ List.iter import refl;
+ Lib.add_frozen_state ()
let vernac_declare_module export (loc, id) binders_ast mty_ast_o =
(* We check the state of the system (in section, in module type)
@@ -433,9 +417,9 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast_o =
Modintern.interp_modtype Modintern.interp_modexpr
id binders_ast (Some mty_ast_o) None
in
- Modintern.dump_moddef loc mp "mod";
- if_verbose message ("Module "^ string_of_id id ^" is declared");
- Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+ Dumpglob.dump_moddef loc mp "mod";
+ if_verbose message ("Module "^ string_of_id id ^" is declared");
+ Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
(* We check the state of the system (in section, in module type)
@@ -453,7 +437,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
let mp = Declaremods.start_module Modintern.interp_modtype export
id binders_ast mty_ast_o
in
- Modintern.dump_moddef loc mp "mod";
+ Dumpglob.dump_moddef loc mp "mod";
if_verbose message
("Interactive Module "^ string_of_id id ^" started") ;
List.iter
@@ -473,7 +457,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
Modintern.interp_modtype Modintern.interp_modexpr
id binders_ast mty_ast_o mexpr_ast_o
in
- Modintern.dump_moddef loc mp "mod";
+ Dumpglob.dump_moddef loc mp "mod";
if_verbose message
("Module "^ string_of_id id ^" is defined");
Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
@@ -481,9 +465,9 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_o =
let vernac_end_module export (loc,id) =
let mp = Declaremods.end_module id in
- Modintern.dump_modref loc mp "mod";
- if_verbose message ("Module "^ string_of_id id ^" is defined") ;
- Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+ Dumpglob.dump_modref loc mp "mod";
+ if_verbose message ("Module "^ string_of_id id ^" is defined") ;
+ Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
@@ -499,7 +483,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
(idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
([],[]) in
let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast in
- Modintern.dump_moddef loc mp "modtype";
+ Dumpglob.dump_moddef loc mp "modtype";
if_verbose message
("Interactive Module Type "^ string_of_id id ^" started");
List.iter
@@ -509,25 +493,25 @@ let vernac_declare_module_type (loc,id) binders_ast mty_ast_o =
) argsexport
| Some base_mty ->
- let binders_ast = List.map
- (fun (export,idl,ty) ->
- if export <> None then
- error ("Arguments of a functor definition can be imported only if" ^
- " the definition is interactive. Remove the \"Export\" " ^
- "and \"Import\" keywords from every functor argument.")
- else (idl,ty)) binders_ast in
- let mp = Declaremods.declare_modtype Modintern.interp_modtype
+ let binders_ast = List.map
+ (fun (export,idl,ty) ->
+ if export <> None then
+ error ("Arguments of a functor definition can be imported only if" ^
+ " the definition is interactive. Remove the \"Export\" " ^
+ "and \"Import\" keywords from every functor argument.")
+ else (idl,ty)) binders_ast in
+ let mp = Declaremods.declare_modtype Modintern.interp_modtype
id binders_ast base_mty in
- Modintern.dump_moddef loc mp "modtype";
- if_verbose message
- ("Module Type "^ string_of_id id ^" is defined")
+ Dumpglob.dump_moddef loc mp "modtype";
+ if_verbose message
+ ("Module Type "^ string_of_id id ^" is defined")
let vernac_end_modtype (loc,id) =
let mp = Declaremods.end_modtype id in
- Modintern.dump_modref loc mp "modtype";
- if_verbose message
- ("Module Type "^ string_of_id id ^" is defined")
+ Dumpglob.dump_modref loc mp "modtype";
+ if_verbose message
+ ("Module Type "^ string_of_id id ^" is defined")
let vernac_include = function
| CIMTE mty_ast ->
@@ -544,7 +528,7 @@ let vernac_record struc binders sort nameopt cfs =
let const = match nameopt with
| None -> add_prefix "Build_" (snd (snd struc))
| Some (_,id as lid) ->
- if !dump then dump_definition lid false "constr"; id in
+ if !dump then Dumpglob.dump_definition lid false "constr"; id in
let sigma = Evd.empty in
let env = Global.env() in
let s = interp_constr sigma env sort in
@@ -553,11 +537,11 @@ let vernac_record struc binders sort nameopt cfs =
| Sort s -> s
| _ -> user_err_loc
(constr_loc sort,"definition_structure", str "Sort expected") in
- if !dump then (
- dump_definition (snd struc) false "rec";
+ if !Flags.dump then (
+ Dumpglob.dump_definition (snd struc) false "rec";
List.iter (fun (_, x) ->
match x with
- | AssumExpr ((loc, Name id), _) -> dump_definition (loc,id) false "proj"
+ | AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
| _ -> ()) cfs);
ignore(Record.definition_structure (struc,binders,cfs,const,s))
@@ -565,13 +549,13 @@ let vernac_record struc binders sort nameopt cfs =
let vernac_begin_section (_, id as lid) =
check_no_pending_proofs ();
- if !Flags.dump then dump_definition lid true "sec";
+ if !Flags.dump then Dumpglob.dump_definition lid true "sec";
Lib.open_section id
let vernac_end_section (loc, id) =
if !Flags.dump then
- dump_reference loc
- (string_of_dirpath (current_dirpath true)) "<>" "sec";
+ Dumpglob.dump_reference loc
+ (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec";
Lib.close_section id
let vernac_end_segment lid =
@@ -586,7 +570,9 @@ let vernac_end_segment lid =
let vernac_require import _ qidl =
let qidl = List.map qualid_of_reference qidl in
- Library.require_library qidl import
+ let modrefl = List.map (fun (_, qid) -> let (_, dp, _) = (Library.locate_qualified_library qid) in dp) qidl in
+ List.iter2 (fun (loc, _) dp -> Dumpglob.dump_libref loc dp "lib") qidl modrefl;
+ Library.require_library qidl import
let vernac_canonical r =
Recordops.declare_canonical_structure (global_with_alias r)
@@ -605,21 +591,21 @@ let vernac_identity_coercion stre id qids qidt =
(* Type classes *)
let vernac_class id par ar sup props =
- if !dump then (
- dump_definition id false "class";
- List.iter (fun (lid, _, _) -> dump_definition lid false "meth") props);
+ if !Flags.dump then (
+ Dumpglob.dump_definition id false "class";
+ List.iter (fun (lid, _, _) -> Dumpglob.dump_definition lid false "meth") props);
Classes.new_class id par ar sup props
let vernac_instance glob sup inst props pri =
- if !dump then dump_constraint inst false "inst";
+ if !Flags.dump then Dumpglob.dump_constraint inst false "inst";
ignore(Classes.new_instance ~global:glob sup inst props pri)
let vernac_context l =
- if !dump then List.iter (fun x -> dump_constraint x true "var") l;
+ if !Flags.dump then List.iter (fun x -> Dumpglob.dump_constraint x true "var") l;
Classes.context l
let vernac_declare_instance id =
- if !dump then dump_definition id false "inst";
+ if !Flags.dump then Dumpglob.dump_definition id false "inst";
Classes.declare_instance false id
(***********)
@@ -754,7 +740,7 @@ let vernac_declare_tactic_definition = Tacinterp.add_tacdef
let vernac_hints = Auto.add_hints
let vernac_syntactic_definition lid =
- dump_definition lid false "syndef";
+ Dumpglob.dump_definition lid false "syndef";
Command.syntax_definition (snd lid)
let vernac_declare_implicits local r = function