diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2012-07-26 10:04:58 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2012-07-26 10:04:58 -0400 |
| commit | dff81b1a774536c0da5e9650855dfbfc37101419 (patch) | |
| tree | 1ae89db4b35c9dc3c8b5a44d0d71094cc7d4a638 /src/elab_env.sml | |
| parent | 7c37a6336fb1a56fee80e94f9e5188c3436102cd (diff) | |
Remove misguided type class optimization
Diffstat (limited to 'src/elab_env.sml')
| -rw-r--r-- | src/elab_env.sml | 25 |
1 files changed, 2 insertions, 23 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml index df031288..f31804f2 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -163,22 +163,6 @@ val subExpInExp = | ((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 @@ fun pushERel (env : env) x t = 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 |