diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-18 15:46:23 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-25 00:28:53 +0200 |
| commit | e8a6467545c2814c9418889201e8be19c0cef201 (patch) | |
| tree | 7f513d854b76b02f52f98ee0e87052c376175a0f /vernac/classes.ml | |
| parent | 30d3515546cf244837c6340b6b87c5f51e68cbf4 (diff) | |
[location] Make location optional in Loc.located
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
Diffstat (limited to 'vernac/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index bdaa3ece6..fb300dbc1 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -77,7 +77,7 @@ let existing_instance glob g info = match class_of_constr Evd.empty (EConstr.of_constr r) with | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob (*FIXME*) (Flags.use_polymorphic_flag ()) c) - | None -> user_err ~loc:(loc_of_reference g) + | None -> user_err ?loc:(loc_of_reference g) ~hdr:"declare_instance" (Pp.str "Constant does not build instances of a declared type class.") @@ -237,7 +237,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p let get_id = function | Ident id' -> id' - | Qualid (loc,id') -> (loc, snd (repr_qualid id')) + | Qualid (loc,id') -> (Loc.tag ?loc @@ snd (repr_qualid id')) in let props, rest = List.fold_left @@ -257,7 +257,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p let (loc, mid) = get_id loc_mid in List.iter (fun (n, _, x) -> if Name.equal n (Name mid) then - Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) x) + Option.iter (fun x -> Dumpglob.add_glob ?loc (ConstRef x)) x) k.cl_projs; c :: props, rest' with Not_found -> |