more bootstrap fixes

Author: Rob23oba

src/Lean/Elab/Open.lean

@@ -76,7 +76,17 @@ def elabOpenDecl [MonadResolveName m] [MonadInfoTree m] (stx : TSyntax ``Parser.
       for ns in nss do
         for ns in (← resolveNamespace ns) do
           activateScoped ns
-    | `(Parser.Command.openDecl| $ns ($ids:identWithOptDot*)) =>
+    | `(Parser.Command.openDecl| $ns:identWithOptDot ($ids:identWithOptDot*)) =>
+      let nss ← resolveNamespace ns
+      for idStx in ids do
+        let declName ← resolveNameUsingNamespacesCore nss idStx
+        if (← getInfoState).enabled then
+          addConstInfo idStx declName
+        addOpenDecl (OpenDecl.explicit idStx.getId declName)
+    -- TODO: remove after stage0 update
+    | `(Parser.Command.openDecl| $x:openOnly) =>
+      let ns : Ident := ⟨x.raw[0]⟩
+      let ids : TSyntaxArray `ident := TSyntaxArray.mk x.raw[2].getArgs
       let nss ← resolveNamespace ns
       for idStx in ids do
         let declName ← resolveNameUsingNamespacesCore nss idStx