diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-23 11:28:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-23 11:30:14 +0200 |
| commit | f0ba692422a8a608ef44964ecf74d8b483c1beb3 (patch) | |
| tree | 91e08dc5fca6358728e5aed5a9f0ab7e9a84b673 /interp/syntax_def.ml | |
| parent | fb9dfa53f2f71ed501be27213600143ee0b7554d (diff) | |
Fix bug #4904: [Import] does not load intermediately unqualified names of aliases.
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 f96d8acc1..d2dcbd92a 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -43,7 +43,7 @@ let is_alias_of_already_visible_name sp = function false let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = - if not (is_alias_of_already_visible_name sp pat) then begin + if not (Int.equal i 1 && is_alias_of_already_visible_name sp pat) then begin Nametab.push_syndef (Nametab.Exactly i) sp kn; match onlyparse with | None -> |