summaryrefslogtreecommitdiff
path: root/src/elab_env.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2014-12-05 19:41:27 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2014-12-05 19:41:27 -0500
commitb6df808b8ff4795f4523c39860070d6153cfad5d (patch)
treeccb61a8d0924daad1ac2f13bd19af21d80581c2b /src/elab_env.sml
parentb50cd7f9ddf5f7d8428ba79a0e336556389ac1c0 (diff)
Move code from last changeset, to improve performance
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r--src/elab_env.sml19
1 files changed, 1 insertions, 18 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 711db166..9fbe7bd7 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -1114,24 +1114,7 @@ and hnormSgn env (all as (sgn, loc)) =
case sgn of
SgnError => all
| SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n))
- | SgnConst sgis =>
- let
- (* This reshuffling was added to avoid some unfortunate unification behavior.
- * In particular, in sub-signature checking, constraints might be unified,
- * even when we don't expect them to be unifiable, deciding on bad values
- * for unification variables and dooming later unification.
- * By putting all the constraints _last_, we allow all the other unifications
- * to happen first, hoping that no unification variables survive to confuse
- * constraint unification. *)
-
- val (constraint, others) = List.partition
- (fn (SgiConstraint _, _) => true
- | _ => false) sgis
- in
- case constraint of
- [] => all
- | _ => (SgnConst (others @ constraint), loc)
- end
+ | SgnConst _ => all
| SgnFun _ => all
| SgnProj (m, ms, x) =>
let