diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-13 00:22:57 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-18 11:02:58 +0200 |
| commit | 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (patch) | |
| tree | c0d688ecee1d04f01f25a121cc3cc6ecabdfa1bc /plugins/funind/functional_principles_types.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/funind/functional_principles_types.mli')
| -rw-r--r-- | plugins/funind/functional_principles_types.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 33aeafef8..97f9acdb3 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -36,5 +36,5 @@ exception No_graph_found val make_scheme : Evd.evar_map ref -> (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list -val build_scheme : (Id.t*Libnames.reference*Sorts.family) list -> unit -val build_case_scheme : (Id.t*Libnames.reference*Sorts.family) -> unit +val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list -> unit +val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family) -> unit |