diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-17 23:40:35 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-25 00:00:43 +0200 |
| commit | 30d3515546cf244837c6340b6b87c5f51e68cbf4 (patch) | |
| tree | 70dd074f483c34e9f71da20edf878062a4b5b3af /toplevel | |
| parent | 84eb5cd72a015c45337a5a6070c5651f56be6e74 (diff) | |
[location] Remove Loc.ghost.
Now it is a private field, locations are optional.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 10 |
2 files changed, 8 insertions, 6 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f5f43ff66..b7065993f 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -185,7 +185,7 @@ let load_vernacular sid = let load_vernacular_obj = ref ([] : string list) let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj let load_vernac_obj () = - let map dir = Qualid (Loc.ghost, qualid_of_string dir) in + let map dir = Qualid (Loc.tag @@ qualid_of_string dir) in Vernacentries.vernac_require None None (List.rev_map map !load_vernacular_obj) let require_prelude () = @@ -200,7 +200,7 @@ let require_list = ref ([] : string list) let add_require s = require_list := s :: !require_list let require () = let () = if !load_init then silently require_prelude () in - let map dir = Qualid (Loc.ghost, qualid_of_string dir) in + let map dir = Qualid (Loc.tag @@ qualid_of_string dir) in Vernacentries.vernac_require None (Some false) (List.rev_map map !require_list) let add_compat_require v = diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 3359a1672..d6bcd2f15 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -146,9 +146,11 @@ let rec interp_vernac sid po (loc,com) = interp com with reraise -> let (reraise, info) = CErrors.push reraise in - let loc' = Option.default Loc.ghost (Loc.get_loc info) in - if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc) - else iraise (reraise, info) + let info = begin + match Loc.get_loc info with + | None -> Loc.add_loc info loc + | Some _ -> info + end in iraise (reraise, info) (* Load a vernac file. CErrors are annotated with file and location *) and load_vernac verbosely sid file = @@ -281,7 +283,7 @@ let compile verbosely f = let wall_clock2 = Unix.gettimeofday () in check_pending_proofs (); Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ()); - Aux_file.record_in_aux_at Loc.ghost "vo_compile_time" + Aux_file.record_in_aux_at "vo_compile_time" (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1)); Aux_file.stop_aux_file (); if !Flags.xml_export then Hook.get f_xml_end_library (); |