From f0ba692422a8a608ef44964ecf74d8b483c1beb3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 23 Aug 2016 11:28:29 +0200 Subject: Fix bug #4904: [Import] does not load intermediately unqualified names of aliases. --- interp/syntax_def.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/syntax_def.ml') 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 -> -- cgit v1.2.3