summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-07-26 10:04:58 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2012-07-26 10:04:58 -0400
commitdff81b1a774536c0da5e9650855dfbfc37101419 (patch)
tree1ae89db4b35c9dc3c8b5a44d0d71094cc7d4a638 /src
parent7c37a6336fb1a56fee80e94f9e5188c3436102cd (diff)
Remove misguided type class optimization
Diffstat (limited to 'src')
-rw-r--r--src/elab_env.sml25
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