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 /pretyping/glob_ops.mli | |
| 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 'pretyping/glob_ops.mli')
| -rw-r--r-- | pretyping/glob_ops.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index ac2118ba7..dae662747 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -20,7 +20,7 @@ val glob_constr_eq : glob_constr -> glob_constr -> bool (** Operations on [glob_constr] *) -val cases_pattern_loc : cases_pattern -> Loc.t +val cases_pattern_loc : cases_pattern -> Loc.t option val cases_predicate_names : tomatch_tuples -> Name.t list @@ -41,7 +41,8 @@ val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit val occur_glob_constr : Id.t -> glob_constr -> bool val free_glob_vars : glob_constr -> Id.t list val bound_glob_vars : glob_constr -> Id.Set.t -val loc_of_glob_constr : glob_constr -> Loc.t +(* Obsolete *) +val loc_of_glob_constr : glob_constr -> Loc.t option val glob_visible_short_qualid : glob_constr -> Id.t list (* Renaming free variables using a renaming map; fails with |