@@ -505,10 +505,12 @@ expandParams dec ps ns tm = en tm
505expandParamsD :: Bool -> -- True = RHS only
505expandParamsD :: Bool -> -- True = RHS only
506 IState ->
506 IState ->
507 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
507 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl
508−expandParamsD False ist dec ps ns (PTy doc syn fc o n ty)
508+expandParamsD rhsonly ist dec ps ns (PTy doc syn fc o n ty)
509− = if n `elem` ns
509+ = if n `elem` ns && (not rhsonly)
510+ then -- trace (show (n, expandParams dec ps ns ty)) $
510− then PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
511+ PTy doc syn fc o (dec n) (piBind ps (expandParams dec ps ns ty))
512+ else --trace (show (n, expandParams dec ps ns ty)) $
511− else PTy doc syn fc o n (expandParams dec ps ns ty)
513+ PTy doc syn fc o n (expandParams dec ps ns ty)
512expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
514expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)
513 = let n' = if n `elem` ns then dec n else n in
515 = let n' = if n `elem` ns then dec n else n in
514 PClauses fc opts n' (map expandParamsC cs)
516 PClauses fc opts n' (map expandParamsC cs)