# HG changeset patch # User Adam Chlipala # Date 1343311498 14400 # Node ID 0de0daab5fbbf8a4e178278e6182ca1b0200ef5b # Parent d28adceef22ac39d1bd6401d0c52c1768bc24712 Remove misguided type class optimization diff -r d28adceef22a -r 0de0daab5fbb src/elab_env.sml --- a/src/elab_env.sml Wed Jul 25 14:04:59 2012 -0400 +++ b/src/elab_env.sml Thu Jul 26 10:04:58 2012 -0400 @@ -163,22 +163,6 @@ | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep) | (ctx, _) => ctx} -val openCon = - U.Con.existsB {kind = fn ((nk, _), k) => - case k of - KRel n => n >= nk - | _ => false, - con = fn ((_, nc), c) => - case c of - CRel n => n >= nc - | _ => false, - bind = fn (all as (nk, nc), b) => - case b of - U.Con.RelK _ => (nk+1, nc) - | U.Con.RelC _ => (nk, nc+1) - | _ => all} - (0, 0) - (* Back to environments *) datatype 'a var' = @@ -855,13 +839,8 @@ let val rule = (nvs, cs, c, (ERel 0, #2 t)) - val class = - if openCon t then - {openRules = rule :: #openRules class, - closedRules = #closedRules class} - else - {closedRules = rule :: #closedRules class, - openRules = #openRules class} + val class = {openRules = rule :: #openRules class, + closedRules = #closedRules class} in CM.insert (classes, f, class) end