diff options
| author | Pierre-Marie Pédrot | 2019-05-27 15:47:46 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-27 17:52:51 +0200 |
| commit | c1dab62a4ee116e20c53b442dd91084b47bced9f (patch) | |
| tree | 044d033a75d2f715dabd0b1d6bb7b80dc07fe75a /checker/check.ml | |
| parent | c371b6f0bc6aa75fb3fe138d2bd52bdd189550b1 (diff) | |
Remove the delayed universe table from object files.
This was virtually dead code. The only place really accessing this data was the
user pretty-printer, but actually the tables were not installed for vanilla vo
files.
In practice, that meant that the only case where an access to this table could
have been triggered would have been to print a term coming from a vio file,
or a vo file generated via vio2vo. In all other cases, the printer would not
have displayed the internal universes. While the latter might be considered
a bug, I am instead convinced that this notion of user-facing internal universes
needs to be handled by another mechanism, the current one making little sense.
The fact it was broken all along without anybody noticing proves my point.
Diffstat (limited to 'checker/check.ml')
| -rw-r--r-- | checker/check.ml | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/checker/check.ml b/checker/check.ml index 76f40dbac2..c5bc59e72a 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -50,6 +50,7 @@ let pr_path sp = type compilation_unit_name = DirPath.t +type seg_univ = Univ.ContextSet.t * bool type seg_proofs = Constr.constr option array type library_t = { @@ -90,7 +91,6 @@ let register_loaded_library m = (* Map from library names to table of opaque terms *) let opaque_tables = ref LibraryMap.empty -let opaque_univ_tables = ref LibraryMap.empty let access_opaque_table dp i = let t = @@ -326,7 +326,7 @@ let intern_from_file ~intern_mode (dir, f) = let ch = System.with_magic_number_check raw_intern_library f in let (sd:summary_disk), _, digest = marshal_in_segment f ch in let (md:library_disk), _, digest = marshal_in_segment f ch in - let (opaque_csts:'a option), _, udg = marshal_in_segment f ch in + let (opaque_csts:seg_univ option), _, udg = marshal_in_segment f ch in let (discharging:'a option), _, _ = marshal_in_segment f ch in let (tasks:'a option), _, _ = marshal_in_segment f ch in let (table:seg_proofs option), pos, checksum = @@ -345,7 +345,7 @@ let intern_from_file ~intern_mode (dir, f) = (str "The file "++str f++str " contains unfinished tasks"); if opaque_csts <> None then begin Flags.if_verbose chk_pp (str " (was a vio file) "); - Option.iter (fun (_,_,b) -> if not b then + Option.iter (fun (_,b) -> if not b then user_err ~hdr:"intern_from_file" (str "The file "++str f++str " is still a .vio")) opaque_csts; @@ -363,13 +363,9 @@ let intern_from_file ~intern_mode (dir, f) = with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph; Option.iter (fun table -> opaque_tables := LibraryMap.add sd.md_name table !opaque_tables) table; - Option.iter (fun (opaque_csts,_,_) -> - opaque_univ_tables := - LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables) - opaque_csts; let extra_cst = Option.default Univ.ContextSet.empty - (Option.map (fun (_,cs,_) -> cs) opaque_csts) in + (Option.map (fun (cs,_) -> cs) opaque_csts) in mk_library sd md f table digest extra_cst let get_deps (dir, f) = |