@@ -141,15 +141,15 @@ elabRecord info syn fc tyn ty cn cty
141 rec = MN 0 "rec"
141 rec = MN 0 "rec"
143 mkp (UN n) = MN 0 ("p_" ++ n)
143 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)
145 mkp (NS n s) = NS (mkp n) s
145 mkp (NS n s) = NS (mkp n) s
147 mkImp (UN n) = UN ("implicit_" ++ n)
147 mkImp (UN n) = UN ("implicit_" ++ n)
148− mkImp (MN 0 n) = MN 0 ("implicit_" ++ n)
148+ mkImp (MN i n) = MN i ("implicit_" ++ n)
149 mkImp (NS n s) = NS (mkImp n) s
149 mkImp (NS n s) = NS (mkImp n) s
151 mkSet (UN n) = UN ("set_" ++ n)
151 mkSet (UN n) = UN ("set_" ++ n)
152− mkSet (MN 0 n) = MN 0 ("set_" ++ n)
152+ mkSet (MN i n) = MN i ("set_" ++ n)
153 mkSet (NS n s) = NS (mkSet n) s
153 mkSet (NS n s) = NS (mkSet n) s
155 mkProj recty substs cimp ((pn_in, pty), pos)
155 mkProj recty substs cimp ((pn_in, pty), pos)