diff options
| author | Lysxia | 2020-04-19 09:47:13 -0400 |
|---|---|---|
| committer | Lysxia | 2020-04-19 09:47:13 -0400 |
| commit | 8d3f4fcd162c7dd23619f605d55e9a773c131e0e (patch) | |
| tree | 4cffc5a5e6268006249efe398129c582b94788f8 /vernac/record.ml | |
| parent | f3af9a4c6e6813f32dfe632209e145ffbf5fed98 (diff) | |
| parent | 1b344958231af8fadfd2b45316f27e8626bae4b6 (diff) | |
Merge PR #12033: Let coqdoc be informed by coq about binding variables (incidentally fixes #7697)
Reviewed-by: Lysxia
Diffstat (limited to 'vernac/record.ml')
| -rw-r--r-- | vernac/record.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index 0b6e8cd8c1..9fda98d08e 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -71,7 +71,7 @@ let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l = let impls = match i with | Anonymous -> impls - | Name id -> Id.Map.add id (compute_internalization_data env sigma Constrintern.Method t' impl) impls + | Name id -> Id.Map.add id (compute_internalization_data env sigma id Constrintern.Method t' impl) impls in let d = match b' with | None -> LocalAssum (make_annot i r,t') |