diff options
| author | Maxime Dénès | 2018-06-13 00:22:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-18 11:02:58 +0200 |
| commit | 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (patch) | |
| tree | c0d688ecee1d04f01f25a121cc3cc6ecabdfa1bc /plugins/ltac/tacentries.mli | |
| parent | f08153148b3ca0de01e5d7c68d5b318a2cae6d0d (diff) | |
Remove reference name type.
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
Diffstat (limited to 'plugins/ltac/tacentries.mli')
| -rw-r--r-- | plugins/ltac/tacentries.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 3f804ee8d1..2bfbbe2e16 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -65,7 +65,7 @@ val create_ltac_quotation : string -> val print_ltacs : unit -> unit (** Display the list of ltac definitions currently available. *) -val print_located_tactic : Libnames.reference -> unit +val print_located_tactic : Libnames.qualid -> unit (** Display the absolute name of a tactic. *) type _ ty_sig = |