From 3f2742b2c3fd48706d4bfd8bffdd4ae07a338bbd Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 6 Apr 2020 10:04:42 +0200
Subject: 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.
---
 interp/dumpglob.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/dumpglob.mli')

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
-- 
cgit v1.2.3