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.ml | |
| 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.ml')
| -rw-r--r-- | interp/dumpglob.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index e659a5ac5c..57ec708b07 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -246,8 +246,6 @@ let add_glob_kn ?loc kn = let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in add_glob_gen ?loc sp lib_dp "syndef" -let dump_binding ?loc id = () - let dump_def ?loc ty secpath id = Option.iter (fun loc -> if !glob_output = Feedback then Feedback.feedback (Feedback.GlobDef (loc, id, secpath, ty)) @@ -275,3 +273,6 @@ let dump_notation (loc,(df,_)) sc sec = Option.iter (fun loc -> let location = (Loc.make_loc (i, i+1)) in dump_def ~loc:location "not" (Names.DirPath.to_string (Lib.current_dirpath sec)) (cook_notation df sc) ) loc + +let dump_binding ?loc uid = + dump_def ?loc "binder" "<>" uid |