@@ -222,7 +222,7 @@ genAll i args
222 pimp (sUN "B") Placeholder True] ++
222 pimp (sUN "B") Placeholder True] ++
223 [pexp l, pexp r]) o
223 [pexp l, pexp r]) o
224 otherPats o@(PDPair fc hls p t _ v)
224 otherPats o@(PDPair fc hls p t _ v)
225− = ops fc (sUN "Ex_intro")
225+ = ops fc sigmaCon
226 ([pimp (sUN "a") Placeholder True,
226 ([pimp (sUN "a") Placeholder True,
227 pimp (sUN "P") Placeholder True] ++
227 pimp (sUN "P") Placeholder True] ++
228 [pexp t,pexp v]) o
228 [pexp t,pexp v]) o
@@ -243,8 +243,8 @@ genAll i args
243 getExpTm t = getTm t
243 getExpTm t = getTm t
245 -- put it back to its original form
245 -- put it back to its original form
246− resugar (PApp _ (PRef fc hl (UN ei)) [_,_,t,v])
246+ resugar (PApp _ (PRef fc hl n) [_,_,t,v])
247− | ei == txt "Ex_intro"
247+ | n == sigmaCon
248 = PDPair fc [] TypeOrTerm (getTm t) Placeholder (getTm v)
248 = PDPair fc [] TypeOrTerm (getTm t) Placeholder (getTm v)
249 resugar (PApp _ (PRef fc hl n) [_,_,l,r])
249 resugar (PApp _ (PRef fc hl n) [_,_,l,r])
250 | n == pairCon
250 | n == pairCon