diff options
| author | coqbot-app[bot] | 2021-01-09 12:34:12 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-09 12:34:12 +0000 |
| commit | 723440611965ccdecfd56e61c8f1f8618a08841d (patch) | |
| tree | 9d3582f11361a788c7f60568fb95d112839eec1e /interp/syntax_def.ml | |
| parent | 7b946aa196490be8790cd5b46d0860b3bf6e33e1 (diff) | |
| parent | 70d557994583bd081787e28f68d627a0833eb9c0 (diff) | |
Merge PR #13299: Remember universe instances of constants in notations
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Diffstat (limited to 'interp/syntax_def.ml')
| -rw-r--r-- | interp/syntax_def.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index f3ad3546ff..39e628883a 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -40,7 +40,7 @@ let load_syntax_constant i ((sp,kn),(_local,syndef)) = Nametab.push_syndef (Nametab.Until i) sp kn let is_alias_of_already_visible_name sp = function - | _,NRef ref -> + | _,NRef (ref,_) -> let (dir,id) = repr_qualid (Nametab.shortest_qualid_of_global Id.Set.empty ref) in DirPath.is_empty dir && Id.equal id (basename sp) | _ -> |