diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/discharge.ml | 2 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 2 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 16 |
4 files changed, 14 insertions, 7 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index d148a53435..5f2c068fdb 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -323,6 +323,6 @@ let close_section _ s = (process_item oldenv olddir full_olddir newdir) ([],[],([],[],[])) decls in let ids = last_section_hyps olddir in - Summary.unfreeze_lost_summaries fs; + Summary.section_unfreeze_summaries fs; catch_not_found (List.iter process_operation) (List.rev ops); Nametab.push_dir (Until 1) full_olddir (DirClosedSection full_olddir) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e7402cbc63..f9d927f627 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -86,6 +86,7 @@ let _ = { freeze_function = Esyntax.freeze; unfreeze_function = Esyntax.unfreeze; init_function = Esyntax.init; + survive_module = false; survive_section = false } (* Pretty-printing objects = syntax_entry *) @@ -121,6 +122,7 @@ let _ = { freeze_function = Egrammar.freeze; unfreeze_function = Egrammar.unfreeze; init_function = Egrammar.init; + survive_module = false; survive_section = false } (* Tokens *) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index df40b6aa35..56d49d1bf4 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -249,6 +249,7 @@ let _ = { Summary.freeze_function = (fun () -> List.rev (get_loaded_modules())); Summary.unfreeze_function = (fun x -> unfreeze_ml_modules x); Summary.init_function = (fun () -> init_ml_modules ()); + Summary.survive_module = false; Summary.survive_section = true } (* Same as restore_ml_modules, but verbosely *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index dc9b2663e5..9d20226b7a 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -528,11 +528,15 @@ let vernac_require import _ qidl = else raise e -let vernac_import export qidl = - let qidl = List.map qualid_of_reference qidl in - if export then - List.iter Library.export_library qidl - else +let vernac_import export refl = + let import_one ref = + let qid = qualid_of_reference ref in + Library.import_library export qid + in + List.iter import_one refl; + Lib.add_frozen_state () + +(* else let import (loc,qid) = try let mp = Nametab.locate_module qid in @@ -543,7 +547,7 @@ let vernac_import export qidl = str ((string_of_qualid qid)^" is not a module")) in List.iter import qidl; - Lib.add_frozen_state () +*) let vernac_canonical locqid = Recordobj.objdef_declare (Nametab.global locqid) |