@@ -141,15 +141,15 @@ elabRecord info syn fc tyn ty cn cty
141141 rec = MN 0 "rec"
142142
143143 mkp (UN n) = MN 0 ("p_" ++ n)
144− mkp (MN 0 n) = MN 0 ("p_" ++ n)
144+ mkp (MN i n) = MN i ("p_" ++ n)
145145 mkp (NS n s) = NS (mkp n) s
146146
147147 mkImp (UN n) = UN ("implicit_" ++ n)
148− mkImp (MN 0 n) = MN 0 ("implicit_" ++ n)
148+ mkImp (MN i n) = MN i ("implicit_" ++ n)
149149 mkImp (NS n s) = NS (mkImp n) s
150150
151151 mkSet (UN n) = UN ("set_" ++ n)
152− mkSet (MN 0 n) = MN 0 ("set_" ++ n)
152+ mkSet (MN i n) = MN i ("set_" ++ n)
153153 mkSet (NS n s) = NS (mkSet n) s
154154
155155 mkProj recty substs cimp ((pn_in, pty), pos)