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/constrintern.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/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index efbe7ec910..2eb96aad56 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -55,7 +55,7 @@ type internalization_env = var_internalization_data Id.Map.t val empty_internalization_env : internalization_env -val compute_internalization_data : env -> evar_map -> var_internalization_type -> +val compute_internalization_data : env -> evar_map -> Id.t -> var_internalization_type -> types -> Impargs.manual_implicits -> var_internalization_data val compute_internalization_env : env -> evar_map -> ?impls:internalization_env -> var_internalization_type -> |