diff options
| author | Hugo Herbelin | 2020-04-06 10:04:42 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-15 19:45:39 +0200 |
| commit | 3f2742b2c3fd48706d4bfd8bffdd4ae07a338bbd (patch) | |
| tree | 929fd96fd18402056024df6670e1ed92454f2db2 /interp/dumpglob.mli | |
| parent | 79ccbe6b2b73409d7ce5e0e5797320b6e2fd0dd2 (diff) | |
Coqdoc: Exporting location and unique id for binding variables.
This provides linking, appropriate coloring and appropriate hovering
in coqdoc documents.
In particular, this fixes #7697.
Diffstat (limited to 'interp/dumpglob.mli')
| -rw-r--r-- | interp/dumpglob.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index 5409b20472..14e5a81308 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -36,7 +36,7 @@ val dump_secvar : ?loc:Loc.t -> Names.Id.t -> unit val dump_libref : ?loc:Loc.t -> Names.DirPath.t -> string -> unit val dump_notation_location : (int * int) list -> Constrexpr.notation -> (Notation.notation_location * Notation_term.scope_name option) -> unit -val dump_binding : ?loc:Loc.t -> Names.Id.Set.elt -> unit +val dump_binding : ?loc:Loc.t -> string -> unit val dump_notation : (Constrexpr.notation * Notation.notation_location) Loc.located -> Notation_term.scope_name option -> bool -> unit |