@@ -1854,13 +1854,12 @@ addImpl' inpat env infns imp_meths ist ptm
1854 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1854 sc' = ai inpat qq ((n, Just ty):env) ds sc in
1855 PLam fc n nfc ty' sc'
1855 PLam fc n nfc ty' sc'
1856 ai inpat qq env ds (PLet fc n nfc ty val sc)
1856 ai inpat qq env ds (PLet fc n nfc ty val sc)
1857− = case lookupDef n (tt_ctxt ist) of
1857+ = if canBeDConName n (tt_ctxt ist)
1858+ then ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1858− [] -> let ty' = ai inpat qq env ds ty
1859+ else let ty' = ai inpat qq env ds ty
1859− val' = ai inpat qq env ds val
1860+ val' = ai inpat qq env ds val
1860− sc' = ai inpat qq ((n, Just ty):env) ds sc in
1861+ sc' = ai inpat qq ((n, Just ty):env) ds sc in
1861− PLet fc n nfc ty' val' sc'
1862+ PLet fc n nfc ty' val' sc'
1863− ai inpat qq env ds (PCase fc val [(PRef fc [] n, sc)])
1864 ai inpat qq env ds (PPi p n nfc ty sc)
1863 ai inpat qq env ds (PPi p n nfc ty sc)
1865 = let ty' = ai inpat qq env ds ty
1864 = let ty' = ai inpat qq env ds ty
1866 env' = if n `elem` imp_meths then env
1865 env' = if n `elem` imp_meths then env