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/extraction/extract_env.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/extraction/extract_env.mli')
| -rw-r--r-- | plugins/extraction/extract_env.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 77f1fb5ef..54fde2ca4 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -13,14 +13,14 @@ open Names open Libnames -val simple_extraction : reference -> unit -val full_extraction : string option -> reference list -> unit -val separate_extraction : reference list -> unit +val simple_extraction : qualid -> unit +val full_extraction : string option -> qualid list -> unit +val separate_extraction : qualid list -> unit val extraction_library : bool -> Id.t -> unit (* For the test-suite : extraction to a temporary file + ocamlc on it *) -val extract_and_compile : reference list -> unit +val extract_and_compile : qualid list -> unit (* For debug / external output via coqtop.byte + Drop : *) |