about summary refs log tree commit diff
diff options
context:
space:
mode:
authorNiko Matsakis <niko@alum.mit.edu>2012-07-13 18:43:52 -0700
committerNiko Matsakis <niko@alum.mit.edu>2012-07-14 17:37:20 -0700
commit41a21f053ced3df8fe9acc66cb30fb6005339b3e (patch)
tree12cf2e5e9ba0405e31a0a6abd509b6a5d3f477c4
parent1fbb9d035ddd0c9ae56a91167fda2f100c3987ad (diff)
downloadrust-41a21f053ced3df8fe9acc66cb30fb6005339b3e.tar.gz
rust-41a21f053ced3df8fe9acc66cb30fb6005339b3e.zip
remove typestate from code, tests, and docs
-rw-r--r--doc/rust.md331
-rw-r--r--src/cargo/cargo.rs1
-rw-r--r--src/compiletest/compiletest.rs2
-rw-r--r--src/compiletest/runtest.rs1
-rw-r--r--src/fuzzer/fuzzer.rs14
-rw-r--r--src/libcore/path.rs2
-rw-r--r--src/libcore/result.rs9
-rw-r--r--src/libsyntax/ast.rs78
-rw-r--r--src/libsyntax/ast_util.rs16
-rw-r--r--src/libsyntax/ext/auto_serialize.rs17
-rw-r--r--src/libsyntax/ext/pipes/ast_builder.rs5
-rw-r--r--src/libsyntax/fold.rs44
-rw-r--r--src/libsyntax/parse/classify.rs9
-rw-r--r--src/libsyntax/parse/parser.rs153
-rw-r--r--src/libsyntax/parse/token.rs2
-rw-r--r--src/libsyntax/print/pprust.rs87
-rw-r--r--src/libsyntax/visit.rs41
-rw-r--r--src/rustc/back/rpath.rs16
-rw-r--r--src/rustc/driver/driver.rs3
-rw-r--r--src/rustc/front/test.rs9
-rw-r--r--src/rustc/metadata/tydecode.rs88
-rw-r--r--src/rustc/metadata/tyencode.rs49
-rw-r--r--src/rustc/middle/borrowck/categorization.rs4
-rw-r--r--src/rustc/middle/liveness.rs11
-rw-r--r--src/rustc/middle/resolve.rs15
-rw-r--r--src/rustc/middle/resolve3.rs36
-rw-r--r--src/rustc/middle/trans/base.rs49
-rw-r--r--src/rustc/middle/trans/foreign.rs3
-rw-r--r--src/rustc/middle/trans/reflect.rs1
-rw-r--r--src/rustc/middle/trans/shape.rs1
-rw-r--r--src/rustc/middle/trans/type_of.rs1
-rw-r--r--src/rustc/middle/trans/type_use.rs4
-rw-r--r--src/rustc/middle/tstate/bitvectors.rs186
-rw-r--r--src/rustc/middle/ty.rs169
-rw-r--r--src/rustc/middle/typeck.rs5
-rw-r--r--src/rustc/middle/typeck/astconv.rs13
-rw-r--r--src/rustc/middle/typeck/check.rs132
-rw-r--r--src/rustc/middle/typeck/check/alt.rs2
-rw-r--r--src/rustc/middle/typeck/coherence.rs4
-rw-r--r--src/rustc/middle/typeck/collect.rs9
-rw-r--r--src/rustc/middle/typeck/infer.rs74
-rw-r--r--src/rustc/rustc.rc13
-rw-r--r--src/rustc/util/ppaux.rs36
-rw-r--r--src/rustdoc/unindent_pass.rs2
-rw-r--r--src/test/compile-fail/fn-constraint.rs10
-rw-r--r--src/test/compile-fail/if-check-precond-fail.rs12
-rw-r--r--src/test/compile-fail/impure-pred.rs14
-rw-r--r--src/test/compile-fail/liveness-unused.rs12
-rw-r--r--src/test/compile-fail/loop-pred-constraints.rs16
-rw-r--r--src/test/compile-fail/no-constraint-prop.rs18
-rw-r--r--src/test/compile-fail/nonsense-constraints.rs13
-rw-r--r--src/test/compile-fail/not-a-pred-2.rs14
-rw-r--r--src/test/compile-fail/not-a-pred-check.rs10
-rw-r--r--src/test/compile-fail/not-pred-args.rs11
-rw-r--r--src/test/compile-fail/pred-assign.rs16
-rw-r--r--src/test/compile-fail/pred-on-wrong-slots.rs17
-rw-r--r--src/test/compile-fail/pred-swap.rs16
-rw-r--r--src/test/compile-fail/slot-as-pred.rs12
-rw-r--r--src/test/compile-fail/tstate-and-init.rs7
-rw-r--r--src/test/compile-fail/tstate-block-uninit.rs11
-rw-r--r--src/test/compile-fail/tstate-break-uninit-2.rs16
-rw-r--r--src/test/compile-fail/tstate-break-uninit.rs16
-rw-r--r--src/test/compile-fail/tstate-ctor-unsat.rs25
-rw-r--r--src/test/compile-fail/tstate-fru.rs14
-rw-r--r--src/test/compile-fail/tstate-if-no-else.rs10
-rw-r--r--src/test/compile-fail/tstate-if-with-else.rs14
-rw-r--r--src/test/compile-fail/tstate-loop-constraints.rs19
-rw-r--r--src/test/compile-fail/tstate-or-init.rs7
-rw-r--r--src/test/compile-fail/tstate-return.rs9
-rw-r--r--src/test/compile-fail/tstate-unsat-after-item.rs9
-rw-r--r--src/test/compile-fail/tstate-unsat-in-called-fn-expr.rs9
-rw-r--r--src/test/compile-fail/tstate-unsat-in-fn-expr.rs9
-rw-r--r--src/test/compile-fail/tstate-unsat.rs7
-rw-r--r--src/test/compile-fail/tstate-while-break.rs15
-rw-r--r--src/test/compile-fail/tstate-while-cond.rs7
-rw-r--r--src/test/compile-fail/tstate-while-loop-unsat-constriants.rs16
-rw-r--r--src/test/compile-fail/tstate-while.rs10
-rw-r--r--src/test/run-fail/fn-constraint-claim.rs7
-rw-r--r--src/test/run-fail/fn-constraint.rs9
-rw-r--r--src/test/run-fail/if-check-fail.rs2
-rw-r--r--src/test/run-fail/pred.rs7
-rw-r--r--src/test/run-fail/unwind-check.rs8
-rw-r--r--src/test/run-fail/zip-different-lengths.rs10
-rw-r--r--src/test/run-pass/bug-862.rs7
-rw-r--r--src/test/run-pass/check-pattern-bound.rs9
-rw-r--r--src/test/run-pass/claim-nonterm.rs7
-rw-r--r--src/test/run-pass/constrained-type.rs11
-rw-r--r--src/test/run-pass/constraint-prop-expr-move.rs10
-rw-r--r--src/test/run-pass/constraint-prop-move.rs8
-rw-r--r--src/test/run-pass/constraint-prop-swap.rs8
-rw-r--r--src/test/run-pass/constraint-prop.rs8
-rw-r--r--src/test/run-pass/fn-constraint.rs7
-rw-r--r--src/test/run-pass/if-check-precond.rs11
-rw-r--r--src/test/run-pass/if-check.rs2
-rw-r--r--src/test/run-pass/issue-933.rs2
-rw-r--r--src/test/run-pass/issue-970.rs6
-rw-r--r--src/test/run-pass/non-boolean-pure-fns.rs12
-rw-r--r--src/test/run-pass/pred-check.rs4
-rw-r--r--src/test/run-pass/pred.rs14
-rw-r--r--src/test/run-pass/typestate-transitive.rs7
-rw-r--r--src/test/run-pass/unchecked-predicates.rs39
-rw-r--r--src/test/run-pass/weird-exprs.rs4
-rw-r--r--src/test/run-pass/zip-same-length.rs5
103 files changed, 144 insertions, 2248 deletions
diff --git a/doc/rust.md b/doc/rust.md
index 21d15c8b114..b7d5925def0 100644
--- a/doc/rust.md
+++ b/doc/rust.md
@@ -211,7 +211,7 @@ The keywords in [source files](#source-files) are the following strings:
 ~~~~~~~~ {.keyword}
 alt again assert
 break
-check claim class const copy
+check class const copy
 drop
 else enum export extern
 fail false fn for
@@ -1926,10 +1926,6 @@ an optional reference slot to serve as the function's output, bound to the
 `lval` on the right hand side of the call. If the function eventually returns,
 then the expression completes.
 
-A call expression statically requires that the precondition declared in the
-callee's signature is satisfied by the expression prestate. In this way,
-typestates propagate through function boundaries.
-
 An example of a call expression:
 
 ~~~~
@@ -2354,117 +2350,6 @@ library. It is best to use the macro forms of logging (*#error*,
 when it is changed.
 
 
-### Check expressions
-
-~~~~~~~~{.ebnf .gram}
-check_expr : "check" call_expr ;
-~~~~~~~~
-
-A `check` expression connects dynamic assertions made at run-time to the
-static [typestate system](#typestate-system). A `check` expression takes a
-constraint to check at run-time. If the constraint holds at run-time, control
-passes through the `check` and on to the next expression in the enclosing
-block. If the condition fails to hold at run-time, the `check` expression
-behaves as a `fail` expression.
-
-The typestate algorithm is built around `check` expressions, and in particular
-the fact that control *will not pass* a check expression with a condition that
-fails to hold. The typestate algorithm can therefore assume that the (static)
-postcondition of a `check` expression includes the checked constraint
-itself. From there, the typestate algorithm can perform dataflow calculations
-on subsequent expressions, propagating [conditions](#conditions) forward and
-statically comparing implied states and their specifications.
-
-~~~~~~~~
-# fn print(i: int) { }
-
-pure fn even(x: int) -> bool {
-    ret x & 1 == 0;
-}
-
-fn print_even(x: int) : even(x) {
-    print(x);
-}
-
-fn test() {
-    let y: int = 8;
-
-    // Cannot call print_even(y) here.
-
-    check even(y);
-
-    // Can call print_even(y) here, since even(y) now holds.
-    print_even(y);
-}
-~~~~~~~~
-
-### Prove expressions
-
-**Note: Prove expressions are not yet supported by the compiler.**
-
-~~~~~~~~{.ebnf .gram}
-prove_expr : "prove" call_expr ;
-~~~~~~~~
-
-A `prove` expression has no run-time effect. Its purpose is to statically
-check (and document) that its argument constraint holds at its expression
-entry point. If its argument typestate does not hold, under the typestate
-algorithm, the program containing it will fail to compile.
-
-### Claim expressions
-
-~~~~~~~~{.ebnf .gram}
-claim_expr : "claim" call_expr ;
-~~~~~~~~
-
-A `claim` expression is an unsafe variant on a `check` expression that is not
-actually checked at runtime. Thus, using a `claim` implies a proof obligation
-to ensure---without compiler assistance---that an assertion always holds.
-
-Setting a runtime flag can turn all `claim` expressions into `check`
-expressions in a compiled Rust program, but the default is to not check the
-assertion contained in a `claim`. The idea behind `claim` is that performance
-profiling might identify a few bottlenecks in the code where actually checking
-a given callee's predicate is too expensive; `claim` allows the code to
-typecheck without removing the predicate check at every other call site.
-
-
-
-### If-Check expressions
-
-An `if check` expression combines a `if` expression and a `check`
-expression in an indivisible unit that can be used to build more complex
-conditional control-flow than the `check` expression affords.
-
-In fact, `if check` is a "more primitive" expression than `check`;
-instances of the latter can be rewritten as instances of the former. The
-following two examples are equivalent:
-
-Example using `check`:
-
-~~~~
-# pure fn even(x: int) -> bool { true }
-# fn print_even(x: int) { }
-# let x = 0;
-
-check even(x);
-print_even(x);
-~~~~
-
-Equivalent example using `if check`:
-
-~~~~
-# pure fn even(x: int) -> bool { true }
-# fn print_even(x: int) { }
-# let x = 0;
-
-if check even(x) {
-    print_even(x);
-} else {
-    fail;
-}
-~~~~
-
 ### Assert expressions
 
 ~~~~~~~~{.ebnf .gram}
@@ -2813,220 +2698,6 @@ Sending operations are not part of the Rust language, but are
 implemented in the library. Generic functions that send values bound
 the kind of these values to sendable.
 
-
-
-## Typestate system
-
-
-Rust programs have a static semantics that determine the types of values
-produced by each expression, as well as the *predicates* that hold over
-slots in the environment at each point in time during execution.
-
-The latter semantics -- the dataflow analysis of predicates holding over slots
--- is called the *typestate* system.
-
-### Points
-
-Control flows from statement to statement in a block, and through the
-evaluation of each expression, from one sub-expression to another. This
-sequential control flow is specified as a set of _points_, each of which
-has a set of points before and after it in the implied control flow.
-
-For example, this code:
-
-~~~~~~~~
-# let mut s;
-
-s = ~"hello, world";
-io::println(s);
-~~~~~~~~
-
-Consists of 2 statements, 3 expressions and 12 points:
-
-
-* the point before the first statement
-* the point before evaluating the static initializer `"hello, world"`
-* the point after evaluating the static initializer `"hello, world"`
-* the point after the first statement
-* the point before the second statement
-* the point before evaluating the function value `println`
-* the point after evaluating the function value `println`
-* the point before evaluating the arguments to `println`
-* the point before evaluating the symbol `s`
-* the point after evaluating the symbol `s`
-* the point after evaluating the arguments to `println`
-* the point after the second statement
-
-
-Whereas this code:
-
-
-~~~~~~~~
-# fn x() -> ~str { ~"" }
-# fn y() -> ~str { ~"" }
-
-io::println(x() + y());
-~~~~~~~~
-
-Consists of 1 statement, 7 expressions and 14 points:
-
-
-* the point before the statement
-* the point before evaluating the function value `println`
-* the point after evaluating the function value `println`
-* the point before evaluating the arguments to `println`
-* the point before evaluating the arguments to `+`
-* the point before evaluating the function value `x`
-* the point after evaluating the function value `x`
-* the point before evaluating the arguments to `x`
-* the point after evaluating the arguments to `x`
-* the point before evaluating the function value `y`
-* the point after evaluating the function value `y`
-* the point before evaluating the arguments to `y`
-* the point after evaluating the arguments to `y`
-* the point after evaluating the arguments to `+`
-* the point after evaluating the arguments to `println`
-
-
-The typestate system reasons over points, rather than statements or
-expressions. This may seem counter-intuitive, but points are the more
-primitive concept. Another way of thinking about a point is as a set of
-*instants in time* at which the state of a task is fixed. By contrast, a
-statement or expression represents a *duration in time*, during which the
-state of the task changes. The typestate system is concerned with constraining
-the possible states of a task's memory at *instants*; it is meaningless to
-speak of the state of a task's memory "at" a statement or expression, as each
-statement or expression is likely to change the contents of memory.
-
-
-### Control flow graph
-
-Each *point* can be considered a vertex in a directed *graph*. Each
-kind of expression or statement implies a number of points *and edges* in
-this graph. The edges connect the points within each statement or expression,
-as well as between those points and those of nearby statements and expressions
-in the program. The edges between points represent *possible* indivisible
-control transfers that might occur during execution.
-
-This implicit graph is called the _control-flow graph_, or _CFG_.
-
-
-### Constraints
-
-A [_predicate_](#predicate-functions) is a pure boolean function declared with
-the keywords `pure fn`.
-
-A _constraint_ is a predicate applied to specific slots.
-
-For example, consider the following code:
-
-~~~~~~~~
-pure fn is_less_than(a: int, b: int) -> bool {
-     ret a < b;
-}
-
-fn test() {
-   let x: int = 10;
-   let y: int = 20;
-   check is_less_than(x,y);
-}
-~~~~~~~~
-
-This example defines the predicate `is_less_than`, and applies it to the slots
-`x` and `y`. The constraint being checked on the third line of the function is
-`is_less_than(x,y)`.
-
-Predicates can only apply to slots holding immutable values. The slots a
-predicate applies to can themselves be mutable, but the types of values held
-in those slots must be immutable.
-
-### Conditions
-
-A _condition_ is a set of zero or more constraints.
-
-Each *point* has an associated *condition*:
-
-* The _precondition_ of a statement or expression is the condition required at
-in the point before it.
-* The _postcondition_ of a statement or expression is the condition enforced
-in the point after it.
-
-Any constraint present in the precondition and *absent* in the postcondition
-is considered to be *dropped* by the statement or expression.
-
-
-### Calculated typestates
-
-The typestate checking system *calculates* an additional condition for each
-point called its _typestate_. For a given statement or expression, we call the
-two typestates associated with its two points the prestate and a poststate.
-
-* The _prestate_ of a statement or expression is the typestate of the
-point before it.
-* The _poststate_ of a statement or expression is the typestate of the
-point after it.
-
-A _typestate_ is a condition that has _been determined by the typestate
-algorithm_ to hold at a point. This is a subtle but important point to
-understand: preconditions and postconditions are *inputs* to the typestate
-algorithm; prestates and poststates are *outputs* from the typestate
-algorithm.
-
-The typestate algorithm analyses the preconditions and postconditions of every
-statement and expression in a block, and computes a condition for each
-typestate. Specifically:
-
-
-* Initially, every typestate is empty.
-* Each statement or expression's poststate is given the union of the its
-prestate, precondition, and postcondition.
-* Each statement or expression's poststate has the difference between its
-precondition and postcondition removed.
-* Each statement or expression's prestate is given the intersection of the
-poststates of every predecessor point in the CFG.
-* The previous three steps are repeated until no typestates in the
-block change.
-
-The typestate algorithm is a very conventional dataflow calculation, and can
-be performed using bit-set operations, with one bit per predicate and one
-bit-set per condition.
-
-After the typestates of a block are computed, the typestate algorithm checks
-that every constraint in the precondition of a statement is satisfied by its
-prestate. If any preconditions are not satisfied, the mismatch is considered a
-static (compile-time) error.
-
-
-### Typestate checks
-
-The key mechanism that connects run-time semantics and compile-time analysis
-of typestates is the use of [`check` expressions](#check-expressions). A
-`check` expression guarantees that *if* control were to proceed past it, the
-predicate associated with the `check` would have succeeded, so the constraint
-being checked *statically* holds in subsequent points.^[A `check` expression
-is similar to an `assert` call in a C program, with the significant difference
-that the Rust compiler *tracks* the constraint that each `check` expression
-enforces. Naturally, `check` expressions cannot be omitted from a "production
-build" of a Rust program the same way `asserts` are frequently disabled in
-deployed C programs.}
-
-It is important to understand that the typestate system has *no insight* into
-the meaning of a particular predicate. Predicates and constraints are not
-evaluated in any way at compile time. Predicates are treated as specific (but
-unknown) functions applied to specific (also unknown) slots. All the typestate
-system does is track which of those predicates -- whatever they calculate --
-*must have been checked already* in order for program control to reach a
-particular point in the CFG. The fundamental building block, therefore, is the
-`check` statement, which tells the typestate system "if control passes this
-point, the checked predicate holds".
-
-From this building block, constraints can be propagated to function signatures
-and constrained types, and the responsibility to `check` a constraint
-pushed further and further away from the site at which the program requires it
-to hold in order to execute properly.
-
-
-
 # Memory and concurrency models
 
 Rust has a memory model centered around concurrently-executing _tasks_. Thus
diff --git a/src/cargo/cargo.rs b/src/cargo/cargo.rs
index 6b9b6c9c39d..0ac7cf00874 100644
--- a/src/cargo/cargo.rs
+++ b/src/cargo/cargo.rs
@@ -763,7 +763,6 @@ fn rustc_sysroot() -> ~str {
     alt os::self_exe_path() {
         some(path) {
             let path = ~[path, ~"..", ~"bin", ~"rustc"];
-            check vec::is_not_empty(path);
             let rustc = path::normalize(path::connect_many(path));
             #debug("  rustc: %s", rustc);
             rustc
diff --git a/src/compiletest/compiletest.rs b/src/compiletest/compiletest.rs
index 30adf8ba5bb..3ba358bfb93 100644
--- a/src/compiletest/compiletest.rs
+++ b/src/compiletest/compiletest.rs
@@ -39,7 +39,7 @@ fn parse_config(args: ~[~str]) -> config {
           getopts::optflag(~"verbose"),
           getopts::optopt(~"logfile")];
 
-    check (vec::is_not_empty(args));
+    assert (vec::is_not_empty(args));
     let args_ = vec::tail(args);
     let match =
         alt getopts::getopts(args_, opts) {
diff --git a/src/compiletest/runtest.rs b/src/compiletest/runtest.rs
index cd8bcb79a9a..6e43c1756a7 100644
--- a/src/compiletest/runtest.rs
+++ b/src/compiletest/runtest.rs
@@ -121,7 +121,6 @@ fn run_pretty_test(config: config, props: test_props, testfile: ~str) {
     if option::is_some(props.pp_exact) {
         // Now we have to care about line endings
         let cr = ~"\r";
-        check (str::is_not_empty(cr));
         actual = str::replace(actual, cr, ~"");
         expected = str::replace(expected, cr, ~"");
     }
diff --git a/src/fuzzer/fuzzer.rs b/src/fuzzer/fuzzer.rs
index 047d6433915..a75f920cfd8 100644
--- a/src/fuzzer/fuzzer.rs
+++ b/src/fuzzer/fuzzer.rs
@@ -69,7 +69,6 @@ pure fn safe_to_use_expr(e: ast::expr, tm: test_mode) -> bool {
           // position, the pretty-printer can't preserve this even by
           // parenthesizing!!  See email to marijn.
           ast::expr_if(_, _, _) { false }
-          ast::expr_if_check(_, _, _) { false }
           ast::expr_block(_) { false }
           ast::expr_alt(_, _, _) { false }
           ast::expr_while(_, _) { false }
@@ -87,10 +86,6 @@ pure fn safe_to_use_expr(e: ast::expr, tm: test_mode) -> bool {
           // https://github.com/mozilla/rust/issues/953
           ast::expr_fail(option::some(_)) { false }
 
-          // https://github.com/mozilla/rust/issues/927
-          //ast::expr_assert(_) { false }
-          ast::expr_check(_, _) { false }
-
           // https://github.com/mozilla/rust/issues/928
           //ast::expr_cast(_, _) { false }
 
@@ -105,13 +100,8 @@ pure fn safe_to_use_expr(e: ast::expr, tm: test_mode) -> bool {
 }
 
 fn safe_to_steal_ty(t: @ast::ty, tm: test_mode) -> bool {
-    alt t.node {
-        // https://github.com/mozilla/rust/issues/971
-        ast::ty_constr(_, _) { false }
-
-        // Other restrictions happen to be the same.
-        _ { safe_to_replace_ty(t.node, tm) }
-    }
+    // Restrictions happen to be the same.
+    safe_to_replace_ty(t.node, tm)
 }
 
 // Not type-parameterized: https://github.com/mozilla/rust/issues/898 (FIXED)
diff --git a/src/libcore/path.rs b/src/libcore/path.rs
index cac66e15095..8331284bf10 100644
--- a/src/libcore/path.rs
+++ b/src/libcore/path.rs
@@ -217,7 +217,7 @@ fn normalize(p: path) -> path {
     let s = strip_dots(s);
     let s = rollup_doubledots(s);
 
-    let s = if check vec::is_not_empty(s) {
+    let s = if vec::is_not_empty(s) {
         connect_many(s)
     } else {
         ~""
diff --git a/src/libcore/result.rs b/src/libcore/result.rs
index c0c68459fb6..0abf3ce299b 100644
--- a/src/libcore/result.rs
+++ b/src/libcore/result.rs
@@ -289,9 +289,9 @@ fn map_opt<T,U:copy,V:copy>(
  * to accommodate an error like the vectors being of different lengths.
  */
 fn map_vec2<S,T,U:copy,V:copy>(ss: ~[S], ts: ~[T],
-                               op: fn(S,T) -> result<V,U>)
-    : vec::same_length(ss, ts) -> result<~[V],U> {
+                               op: fn(S,T) -> result<V,U>) -> result<~[V],U> {
 
+    assert vec::same_length(ss, ts);
     let n = vec::len(ts);
     let mut vs = ~[];
     vec::reserve(vs, n);
@@ -312,10 +312,9 @@ fn map_vec2<S,T,U:copy,V:copy>(ss: ~[S], ts: ~[T],
  * on its own as no result vector is built.
  */
 fn iter_vec2<S,T,U:copy>(ss: ~[S], ts: ~[T],
-                         op: fn(S,T) -> result<(),U>)
-    : vec::same_length(ss, ts)
-    -> result<(),U> {
+                         op: fn(S,T) -> result<(),U>) -> result<(),U> {
 
+    assert vec::same_length(ss, ts);
     let n = vec::len(ts);
     let mut i = 0u;
     while i < n {
diff --git a/src/libsyntax/ast.rs b/src/libsyntax/ast.rs
index 6cf6818ba40..db70ad12b6e 100644
--- a/src/libsyntax/ast.rs
+++ b/src/libsyntax/ast.rs
@@ -285,9 +285,6 @@ type field = spanned<field_>;
 enum blk_check_mode { default_blk, unchecked_blk, unsafe_blk, }
 
 #[auto_serialize]
-enum expr_check_mode { claimed_expr, checked_expr, }
-
-#[auto_serialize]
 type expr = {id: node_id, callee_id: node_id, node: expr_, span: span};
 // Extra node ID is only used for index, assign_op, unary, binary
 
@@ -322,10 +319,6 @@ enum expr_ {
     expr_do_body(@expr),
     expr_block(blk),
 
-    /*
-     * FIXME (#34): many of these @exprs should be constrained with
-     * is_lval once we have constrained types working.
-     */
     expr_copy(@expr),
     expr_move(@expr, @expr),
     expr_assign(@expr, @expr),
@@ -348,9 +341,6 @@ enum expr_ {
     /* just an assert, no significance to typestate */
     expr_assert(@expr),
 
-    /* preds that typestate is aware of */
-    expr_check(expr_check_mode, @expr),
-    expr_if_check(@expr, blk, option<@expr>),
     expr_mac(mac),
 }
 
@@ -365,15 +355,6 @@ type capture_item = @{
 #[auto_serialize]
 type capture_clause = @~[capture_item];
 
-/*
-// Says whether this is a block the user marked as
-// "unchecked"
-enum blk_sort {
-    blk_unchecked, // declared as "exception to effect-checking rules"
-    blk_checked, // all typing rules apply
-}
-*/
-
 #[auto_serialize]
 #[doc="For macro invocations; parsing is delegated to the macro"]
 enum token_tree {
@@ -384,8 +365,6 @@ enum token_tree {
     tt_interpolate(span, ident)
 }
 
-
-
 #[auto_serialize]
 type matcher = spanned<matcher_>;
 
@@ -502,7 +481,6 @@ enum ty_ {
     ty_fn(proto, fn_decl),
     ty_tup(~[@ty]),
     ty_path(@path, node_id),
-    ty_constr(@ty, ~[@ty_constr]),
     ty_fixed_length(@ty, option<uint>),
     ty_mac(mac),
     // ty_infer means the type should be inferred instead of it having been
@@ -511,59 +489,6 @@ enum ty_ {
     ty_infer,
 }
 
-
-/*
-A constraint arg that's a function argument is referred to by its position
-rather than name.  This is so we could have higher-order functions that have
-constraints (potentially -- right now there's no way to write that), and also
-so that the typestate pass doesn't have to map a function name onto its decl.
-So, the constr_arg type is parameterized: it's instantiated with uint for
-declarations, and ident for uses.
-*/
-#[auto_serialize]
-enum constr_arg_general_<T> { carg_base, carg_ident(T), carg_lit(@lit), }
-
-#[auto_serialize]
-type fn_constr_arg = constr_arg_general_<uint>;
-
-#[auto_serialize]
-type sp_constr_arg<T> = spanned<constr_arg_general_<T>>;
-
-#[auto_serialize]
-type ty_constr_arg = sp_constr_arg<@path>;
-
-#[auto_serialize]
-type constr_arg = spanned<fn_constr_arg>;
-
-// Constrained types' args are parameterized by paths, since
-// we refer to paths directly and not by indices.
-// The implicit root of such path, in the constraint-list for a
-// constrained type, is * (referring to the base record)
-
-#[auto_serialize]
-type constr_general_<ARG, ID> =
-    {path: @path, args: ~[@sp_constr_arg<ARG>], id: ID};
-
-// In the front end, constraints have a node ID attached.
-// Typeck turns this to a def_id, using the output of resolve.
-#[auto_serialize]
-type constr_general<ARG> = spanned<constr_general_<ARG, node_id>>;
-
-#[auto_serialize]
-type constr_ = constr_general_<uint, node_id>;
-
-#[auto_serialize]
-type constr = spanned<constr_general_<uint, node_id>>;
-
-#[auto_serialize]
-type ty_constr_ = constr_general_<@path, node_id>;
-
-#[auto_serialize]
-type ty_constr = spanned<ty_constr_>;
-
-/* The parser generates ast::constrs; resolve generates
- a mapping from each function to a list of ty::constr_defs,
- corresponding to these. */
 #[auto_serialize]
 type arg = {mode: mode, ty: @ty, ident: ident, id: node_id};
 
@@ -572,8 +497,7 @@ type fn_decl =
     {inputs: ~[arg],
      output: @ty,
      purity: purity,
-     cf: ret_style,
-     constraints: ~[@constr]};
+     cf: ret_style};
 
 #[auto_serialize]
 enum purity {
diff --git a/src/libsyntax/ast_util.rs b/src/libsyntax/ast_util.rs
index 556239769da..49478779fba 100644
--- a/src/libsyntax/ast_util.rs
+++ b/src/libsyntax/ast_util.rs
@@ -213,14 +213,6 @@ pure fn is_call_expr(e: @expr) -> bool {
     alt e.node { expr_call(_, _, _) { true } _ { false } }
 }
 
-fn is_constraint_arg(e: @expr) -> bool {
-    alt e.node {
-      expr_lit(_) { ret true; }
-      expr_path(_) { ret true; }
-      _ { ret false; }
-    }
-}
-
 fn eq_ty(&&a: @ty, &&b: @ty) -> bool { ret box::ptr_eq(a, b); }
 
 fn hash_ty(&&t: @ty) -> uint {
@@ -381,8 +373,8 @@ fn dtor_dec() -> fn_decl {
     let nil_t = @{id: 0, node: ty_nil, span: dummy_sp()};
     // dtor has one argument, of type ()
     {inputs: ~[{mode: ast::expl(ast::by_ref),
-               ty: nil_t, ident: @~"_", id: 0}],
-     output: nil_t, purity: impure_fn, cf: return_val, constraints: ~[]}
+                ty: nil_t, ident: @~"_", id: 0}],
+     output: nil_t, purity: impure_fn, cf: return_val}
 }
 
 // ______________________________________________________________________
@@ -467,10 +459,6 @@ fn id_visitor(vfn: fn@(node_id)) -> visit::vt<()> {
             vec::iter(ps, |p| vfn(p.id))
         },
 
-        visit_constr: fn@(_p: @path, _sp: span, id: node_id) {
-            vfn(id);
-        },
-
         visit_fn: fn@(fk: visit::fn_kind, d: ast::fn_decl,
                       _b: ast::blk, _sp: span, id: ast::node_id) {
             vfn(id);
diff --git a/src/libsyntax/ext/auto_serialize.rs b/src/libsyntax/ext/auto_serialize.rs
index 98671234249..a7a6080fb0b 100644
--- a/src/libsyntax/ext/auto_serialize.rs
+++ b/src/libsyntax/ext/auto_serialize.rs
@@ -162,8 +162,7 @@ impl helpers for ext_ctxt {
           node: ast::ty_fn(ast::proto_any, {inputs: args,
                                             output: output,
                                             purity: ast::impure_fn,
-                                            cf: ast::return_val,
-                                            constraints: ~[]}),
+                                            cf: ast::return_val}),
           span: span}
     }
 
@@ -466,10 +465,6 @@ fn ser_ty(cx: ext_ctxt, tps: ser_tps_map,
         }
       }
 
-      ast::ty_constr(ty, _) {
-        ser_ty(cx, tps, ty, s, v)
-      }
-
       ast::ty_mac(_) {
         cx.span_err(ty.span, ~"cannot serialize macro types");
         ~[]
@@ -573,8 +568,7 @@ fn mk_ser_fn(cx: ext_ctxt, span: span, name: ast::ident,
       node: ast::item_fn({inputs: ser_inputs,
                           output: ser_output,
                           purity: ast::impure_fn,
-                          cf: ast::return_val,
-                          constraints: ~[]},
+                          cf: ast::return_val},
                          ser_tps,
                          ser_blk),
       vis: ast::public,
@@ -697,10 +691,6 @@ fn deser_ty(cx: ext_ctxt, tps: deser_tps_map,
         }
       }
 
-      ast::ty_constr(ty, constrs) {
-        deser_ty(cx, tps, ty, d)
-      }
-
       ast::ty_mac(_) {
         #ast{ fail }
       }
@@ -783,8 +773,7 @@ fn mk_deser_fn(cx: ext_ctxt, span: span,
       node: ast::item_fn({inputs: deser_inputs,
                           output: v_ty,
                           purity: ast::impure_fn,
-                          cf: ast::return_val,
-                          constraints: ~[]},
+                          cf: ast::return_val},
                          deser_tps,
                          deser_blk),
       vis: ast::public,
diff --git a/src/libsyntax/ext/pipes/ast_builder.rs b/src/libsyntax/ext/pipes/ast_builder.rs
index cb0abe9e8e5..2a2fbe2628a 100644
--- a/src/libsyntax/ext/pipes/ast_builder.rs
+++ b/src/libsyntax/ext/pipes/ast_builder.rs
@@ -89,10 +89,7 @@ impl ast_builder for ext_ctxt {
         {inputs: inputs,
          output: output,
          purity: ast::impure_fn,
-         cf: ast::return_val,
-         // FIXME #2886: we'll probably want a variant that does constrained
-         // types.
-         constraints: ~[]}
+         cf: ast::return_val}
     }
 
     fn item(name: ident,
diff --git a/src/libsyntax/fold.rs b/src/libsyntax/fold.rs
index e3bb29cdb92..965caacf07a 100644
--- a/src/libsyntax/fold.rs
+++ b/src/libsyntax/fold.rs
@@ -33,8 +33,6 @@ iface ast_fold {
     fn fold_decl(&&@decl) -> @decl;
     fn fold_expr(&&@expr) -> @expr;
     fn fold_ty(&&@ty) -> @ty;
-    fn fold_constr(&&@constr) -> @constr;
-    fn fold_ty_constr(&&@ty_constr) -> @ty_constr;
     fn fold_mod(_mod) -> _mod;
     fn fold_foreign_mod(foreign_mod) -> foreign_mod;
     fn fold_variant(variant) -> variant;
@@ -66,9 +64,6 @@ type ast_fold_precursor = @{
     fold_decl: fn@(decl_, span, ast_fold) -> (decl_, span),
     fold_expr: fn@(expr_, span, ast_fold) -> (expr_, span),
     fold_ty: fn@(ty_, span, ast_fold) -> (ty_, span),
-    fold_constr: fn@(ast::constr_, span, ast_fold) -> (constr_, span),
-    fold_ty_constr: fn@(ast::ty_constr_, span, ast_fold)
-        -> (ty_constr_, span),
     fold_mod: fn@(_mod, ast_fold) -> _mod,
     fold_foreign_mod: fn@(foreign_mod, ast_fold) -> foreign_mod,
     fold_variant: fn@(variant_, span, ast_fold) -> (variant_, span),
@@ -135,8 +130,7 @@ fn fold_fn_decl(decl: ast::fn_decl, fld: ast_fold) -> ast::fn_decl {
     ret {inputs: vec::map(decl.inputs, |x| fold_arg_(x, fld) ),
          output: fld.fold_ty(decl.output),
          purity: decl.purity,
-         cf: decl.cf,
-         constraints: vec::map(decl.constraints, |x| fld.fold_constr(x))}
+         cf: decl.cf}
 }
 
 fn fold_ty_param_bound(tpb: ty_param_bound, fld: ast_fold) -> ty_param_bound {
@@ -200,10 +194,7 @@ fn noop_fold_foreign_item(&&ni: @foreign_item, fld: ast_fold)
                   foreign_item_fn({inputs: vec::map(fdec.inputs, fold_arg),
                                   output: fld.fold_ty(fdec.output),
                                   purity: fdec.purity,
-                                  cf: fdec.cf,
-                                  constraints:
-                                      vec::map(fdec.constraints,
-                                               |x| fld.fold_constr(x))},
+                                  cf: fdec.cf},
                                  fold_ty_params(typms, fld))
                 }
               },
@@ -474,11 +465,6 @@ fn noop_fold_expr(e: expr_, fld: ast_fold) -> expr_ {
           expr_log(i, lv, e) { expr_log(i, fld.fold_expr(lv),
                                         fld.fold_expr(e)) }
           expr_assert(e) { expr_assert(fld.fold_expr(e)) }
-          expr_check(m, e) { expr_check(m, fld.fold_expr(e)) }
-          expr_if_check(cond, tr, fl) {
-            expr_if_check(fld.fold_expr(cond), fld.fold_block(tr),
-                          option::map(fl, |x| fld.fold_expr(x)))
-          }
           expr_mac(mac) { expr_mac(fold_mac(mac)) }
         }
 }
@@ -504,24 +490,11 @@ fn noop_fold_ty(t: ty_, fld: ast_fold) -> ty_ {
       ty_fn(proto, decl) {ty_fn(proto, fold_fn_decl(decl, fld))}
       ty_tup(tys) {ty_tup(vec::map(tys, |ty| fld.fold_ty(ty)))}
       ty_path(path, id) {ty_path(fld.fold_path(path), fld.new_id(id))}
-      ty_constr(ty, constrs) {ty_constr(fld.fold_ty(ty),
-                                vec::map(constrs, |x| fld.fold_ty_constr(x)))}
       ty_fixed_length(t, vs) {ty_fixed_length(fld.fold_ty(t), vs)}
       ty_mac(mac) {ty_mac(fold_mac(mac))}
     }
 }
 
-fn noop_fold_constr(c: constr_, fld: ast_fold) -> constr_ {
-    {path: fld.fold_path(c.path), args: /* FIXME (#2543) */ copy c.args,
-     id: fld.new_id(c.id)}
-}
-
-fn noop_fold_ty_constr(c: ty_constr_, fld: ast_fold) -> ty_constr_ {
-    let rslt: ty_constr_ =
-        {path: fld.fold_path(c.path), args: /* FIXME (#2543) */ copy c.args,
-         id: fld.new_id(c.id)};
-    rslt
-}
 // ...nor do modules
 fn noop_fold_mod(m: _mod, fld: ast_fold) -> _mod {
     ret {view_items: vec::map(m.view_items, |x| fld.fold_view_item(x)),
@@ -606,8 +579,6 @@ fn default_ast_fold() -> ast_fold_precursor {
           fold_decl: wrap(noop_fold_decl),
           fold_expr: wrap(noop_fold_expr),
           fold_ty: wrap(noop_fold_ty),
-          fold_constr: wrap(noop_fold_constr),
-          fold_ty_constr: wrap(noop_fold_ty_constr),
           fold_mod: noop_fold_mod,
           fold_foreign_mod: noop_fold_foreign_mod,
           fold_variant: wrap(noop_fold_variant),
@@ -697,17 +668,6 @@ impl of ast_fold for ast_fold_precursor {
         let (n, s) = self.fold_ty(x.node, x.span, self as ast_fold);
         ret @{id: self.new_id(x.id), node: n, span: self.new_span(s)};
     }
-    fn fold_constr(&&x: @ast::constr) ->
-       @ast::constr {
-        let (n, s) = self.fold_constr(x.node, x.span, self as ast_fold);
-        ret @{node: n, span: self.new_span(s)};
-    }
-    fn fold_ty_constr(&&x: @ast::ty_constr) ->
-       @ast::ty_constr {
-        let (n, s) : (ty_constr_, span) =
-            self.fold_ty_constr(x.node, x.span, self as ast_fold);
-        ret @{node: n, span: self.new_span(s)};
-    }
     fn fold_mod(x: _mod) -> _mod {
         ret self.fold_mod(x, self as ast_fold);
     }
diff --git a/src/libsyntax/parse/classify.rs b/src/libsyntax/parse/classify.rs
index 9b36b77407e..20fb7772d08 100644
--- a/src/libsyntax/parse/classify.rs
+++ b/src/libsyntax/parse/classify.rs
@@ -6,8 +6,7 @@ import ast_util::operator_prec;
 
 fn expr_requires_semi_to_be_stmt(e: @ast::expr) -> bool {
     alt e.node {
-      ast::expr_if(_, _, _) | ast::expr_if_check(_, _, _)
-      | ast::expr_alt(_, _, _) | ast::expr_block(_)
+      ast::expr_if(_, _, _) | ast::expr_alt(_, _, _) | ast::expr_block(_)
       | ast::expr_while(_, _) | ast::expr_loop(_)
       | ast::expr_call(_, _, true) {
         false
@@ -44,7 +43,6 @@ fn need_parens(expr: @ast::expr, outer_prec: uint) -> bool {
       ast::expr_assign_op(_, _, _) { true }
       ast::expr_ret(_) { true }
       ast::expr_assert(_) { true }
-      ast::expr_check(_, _) { true }
       ast::expr_log(_, _, _) { true }
       _ { !parse::classify::expr_requires_semi_to_be_stmt(expr) }
     }
@@ -64,8 +62,9 @@ fn ends_in_lit_int(ex: @ast::expr) -> bool {
       ast::expr_move(_, sub) | ast::expr_copy(sub) |
       ast::expr_assign(_, sub) |
       ast::expr_assign_op(_, _, sub) | ast::expr_swap(_, sub) |
-      ast::expr_log(_, _, sub) | ast::expr_assert(sub) |
-      ast::expr_check(_, sub) { ends_in_lit_int(sub) }
+      ast::expr_log(_, _, sub) | ast::expr_assert(sub) {
+        ends_in_lit_int(sub)
+      }
       ast::expr_fail(osub) | ast::expr_ret(osub) {
         alt osub {
           some(ex) { ends_in_lit_int(ex) }
diff --git a/src/libsyntax/parse/parser.rs b/src/libsyntax/parse/parser.rs
index b67fd88ab61..fa0361e797b 100644
--- a/src/libsyntax/parse/parser.rs
+++ b/src/libsyntax/parse/parser.rs
@@ -20,14 +20,14 @@ import ast::{_mod, add, alt_check, alt_exhaustive, arg, arm, attribute,
              by_mutbl_ref, by_ref, by_val, capture_clause, capture_item,
              carg_base, carg_ident, cdir_dir_mod, cdir_src_mod,
              cdir_view_item, checked_expr, claimed_expr, class_immutable,
-             class_member, class_method, class_mutable, constr, constr_arg,
-             constr_general, crate, crate_cfg, crate_directive, decl,
+             class_member, class_method, class_mutable,
+             crate, crate_cfg, crate_directive, decl,
              decl_item, decl_local, default_blk, deref, div, expl, expr,
              expr_, expr_addr_of, expr_alt, expr_again, expr_assert,
              expr_assign, expr_assign_op, expr_binary, expr_block, expr_break,
-             expr_call, expr_cast, expr_check, expr_copy, expr_do_body,
+             expr_call, expr_cast, expr_copy, expr_do_body,
              expr_fail, expr_field, expr_fn, expr_fn_block, expr_if,
-             expr_if_check, expr_index, expr_lit, expr_log, expr_loop,
+             expr_index, expr_lit, expr_log, expr_loop,
              expr_loop_body, expr_mac, expr_move, expr_new, expr_path,
              expr_rec, expr_ret, expr_swap, expr_tup, expr_unary, expr_vec,
              expr_vstore, expr_while, extern_fn, field, fn_decl, foreign_item,
@@ -265,15 +265,9 @@ class parser {
             {mode: mode, ty: p.parse_ty(false), ident: name,
              id: p.get_id()}
         };
-        // FIXME (#34): constrs is empty because right now, higher-order
-        // functions can't have constrained types. Not sure whether
-        // that would be desirable anyway. See bug for the story on
-        // constrained types.
-        let constrs: ~[@constr] = ~[];
         let (ret_style, ret_ty) = self.parse_ret_ty();
         ret {inputs: inputs, output: ret_ty,
-             purity: purity, cf: ret_style,
-             constraints: constrs};
+             purity: purity, cf: ret_style};
     }
 
     fn parse_trait_methods() -> ~[trait_method] {
@@ -341,79 +335,6 @@ class parser {
         ret spanned(lo, ty.span.hi, {ident: id, mt: {ty: ty, mutbl: mutbl}});
     }
 
-    // if i is the jth ident in args, return j
-    // otherwise, fail
-    fn ident_index(args: ~[arg], i: ident) -> uint {
-        let mut j = 0u;
-        for args.each |a| { if a.ident == i { ret j; } j += 1u; }
-        self.fatal(~"unbound variable `" + *i + ~"` in constraint arg");
-    }
-
-    fn parse_type_constr_arg() -> @ty_constr_arg {
-        let sp = self.span;
-        let mut carg = carg_base;
-        self.expect(token::BINOP(token::STAR));
-        if self.token == token::DOT {
-            // "*..." notation for record fields
-            self.bump();
-            let pth = self.parse_path_without_tps();
-            carg = carg_ident(pth);
-        }
-        // No literals yet, I guess?
-        ret @{node: carg, span: sp};
-    }
-
-    fn parse_constr_arg(args: ~[arg]) -> @constr_arg {
-        let sp = self.span;
-        let mut carg = carg_base;
-        if self.token == token::BINOP(token::STAR) {
-            self.bump();
-        } else {
-            let i: ident = self.parse_value_ident();
-            carg = carg_ident(self.ident_index(args, i));
-        }
-        ret @{node: carg, span: sp};
-    }
-
-    fn parse_ty_constr(fn_args: ~[arg]) -> @constr {
-        let lo = self.span.lo;
-        let path = self.parse_path_without_tps();
-        let args = self.parse_unspanned_seq(
-            token::LPAREN, token::RPAREN,
-            seq_sep_trailing_disallowed(token::COMMA),
-            |p| p.parse_constr_arg(fn_args));
-        ret @spanned(lo, self.span.hi,
-                     {path: path, args: args, id: self.get_id()});
-    }
-
-    fn parse_constr_in_type() -> @ty_constr {
-        let lo = self.span.lo;
-        let path = self.parse_path_without_tps();
-        let args: ~[@ty_constr_arg] = self.parse_unspanned_seq(
-            token::LPAREN, token::RPAREN,
-            seq_sep_trailing_disallowed(token::COMMA),
-            |p| p.parse_type_constr_arg());
-        let hi = self.span.lo;
-        let tc: ty_constr_ = {path: path, args: args, id: self.get_id()};
-        ret @spanned(lo, hi, tc);
-    }
-
-
-    fn parse_constrs<T: copy>(pser: fn(parser) -> @constr_general<T>) ->
-        ~[@constr_general<T>] {
-        let mut constrs: ~[@constr_general<T>] = ~[];
-        loop {
-            let constr = pser(self);
-            vec::push(constrs, constr);
-            if self.token == token::COMMA { self.bump(); }
-            else { ret constrs; }
-        };
-    }
-
-    fn parse_type_constraints() -> ~[@ty_constr] {
-        ret self.parse_constrs(|p| p.parse_constr_in_type());
-    }
-
     fn parse_ret_ty() -> (ret_style, @ty) {
         ret if self.eat(token::RARROW) {
             let lo = self.span.lo;
@@ -519,16 +440,7 @@ class parser {
             if vec::len(elems) == 0u {
                 self.unexpected_last(token::RBRACE);
             }
-            let hi = self.span.hi;
-
-            let t = ty_rec(elems);
-            if self.token == token::COLON {
-                self.bump();
-                ty_constr(@{id: self.get_id(),
-                            node: t,
-                            span: mk_sp(lo, hi)},
-                          self.parse_type_constraints())
-            } else { t }
+            ty_rec(elems)
         } else if self.token == token::LBRACKET {
             self.expect(token::LBRACKET);
             let t = ty_vec(self.parse_mt());
@@ -970,21 +882,6 @@ class parser {
             let e = self.parse_expr();
             ex = expr_assert(e);
             hi = e.span.hi;
-        } else if self.eat_keyword(~"check") {
-            /* Should be a predicate (pure boolean function) applied to
-            arguments that are all either slot variables or literals.
-            but the typechecker enforces that. */
-            let e = self.parse_expr();
-            hi = e.span.hi;
-            ex = expr_check(checked_expr, e);
-        } else if self.eat_keyword(~"claim") {
-            /* Same rules as check, except that if check-claims
-            is enabled (a command-line flag), then the parser turns
-            claims into check */
-
-            let e = self.parse_expr();
-            hi = e.span.hi;
-            ex = expr_check(claimed_expr, e);
         } else if self.eat_keyword(~"ret") {
             if can_begin_expr(self.token) {
                 let e = self.parse_expr();
@@ -1457,12 +1354,7 @@ class parser {
         ret lhs;
     }
 
-    fn parse_if_expr_1() ->
-        {cond: @expr,
-         then: blk,
-         els: option<@expr>,
-         lo: uint,
-         hi: uint} {
+    fn parse_if_expr() -> @expr {
         let lo = self.last_span.lo;
         let cond = self.parse_expr();
         let thn = self.parse_block();
@@ -1473,18 +1365,8 @@ class parser {
             els = some(elexpr);
             hi = elexpr.span.hi;
         }
-        ret {cond: cond, then: thn, els: els, lo: lo, hi: hi};
-    }
-
-    fn parse_if_expr() -> @expr {
-        if self.eat_keyword(~"check") {
-            let q = self.parse_if_expr_1();
-            ret self.mk_expr(q.lo, q.hi,
-                             expr_if_check(q.cond, q.then, q.els));
-        } else {
-            let q = self.parse_if_expr_1();
-            ret self.mk_expr(q.lo, q.hi, expr_if(q.cond, q.then, q.els));
-        }
+        let q = {cond: cond, then: thn, els: els, lo: lo, hi: hi};
+        ret self.mk_expr(q.lo, q.hi, expr_if(q.cond, q.then, q.els));
     }
 
     fn parse_fn_expr(proto: proto) -> @expr {
@@ -1520,8 +1402,7 @@ class parser {
                                 span: self.span
                             },
                             purity: impure_fn,
-                            cf: return_val,
-                            constraints: ~[]
+                            cf: return_val
                         }
                     },
                     @~[])
@@ -2083,20 +1964,11 @@ class parser {
         let inputs = either::lefts(args_or_capture_items);
         let capture_clause = @either::rights(args_or_capture_items);
 
-        // Use the args list to translate each bound variable
-        // mentioned in a constraint to an arg index.
-        // Seems weird to do this in the parser, but I'm not sure how else to.
-        let mut constrs = ~[];
-        if self.token == token::COLON {
-            self.bump();
-            constrs = self.parse_constrs(|p| p.parse_ty_constr(inputs));
-        }
         let (ret_style, ret_ty) = self.parse_ret_ty();
         ret ({inputs: inputs,
               output: ret_ty,
               purity: purity,
-              cf: ret_style,
-              constraints: constrs}, capture_clause);
+              cf: ret_style}, capture_clause);
     }
 
     fn parse_fn_block_decl() -> (fn_decl, capture_clause) {
@@ -2118,8 +1990,7 @@ class parser {
         ret ({inputs: either::lefts(inputs_captures),
               output: output,
               purity: impure_fn,
-              cf: return_val,
-              constraints: ~[]},
+              cf: return_val},
              @either::rights(inputs_captures));
     }
 
diff --git a/src/libsyntax/parse/token.rs b/src/libsyntax/parse/token.rs
index 7db5af23266..eb8c5b65fa5 100644
--- a/src/libsyntax/parse/token.rs
+++ b/src/libsyntax/parse/token.rs
@@ -306,7 +306,7 @@ fn restricted_keyword_table() -> hashmap<~str, ()> {
     let keys = ~[
         ~"alt", ~"again", ~"assert",
         ~"break",
-        ~"check", ~"claim", ~"class", ~"const", ~"copy",
+        ~"check", ~"class", ~"const", ~"copy",
         ~"do", ~"drop",
         ~"else", ~"enum", ~"export", ~"extern",
         ~"fail", ~"false", ~"fn", ~"for",
diff --git a/src/libsyntax/print/pprust.rs b/src/libsyntax/print/pprust.rs
index a0ad2647cba..1b9b0ce7f96 100644
--- a/src/libsyntax/print/pprust.rs
+++ b/src/libsyntax/print/pprust.rs
@@ -128,8 +128,7 @@ fn test_fun_to_str() {
                   node: ast::ty_nil,
                   span: ast_util::dummy_sp()},
         purity: ast::impure_fn,
-        cf: ast::return_val,
-        constraints: ~[]
+        cf: ast::return_val
     };
     assert fun_to_str(decl, "a", ~[]) == "fn a()";
 }
@@ -373,11 +372,6 @@ fn print_type_ex(s: ps, &&ty: @ast::ty, print_colons: bool) {
         print_ty_fn(s, some(proto), d, none, none);
       }
       ast::ty_path(path, _) { print_path(s, path, print_colons); }
-      ast::ty_constr(t, cs) {
-        print_type(s, t);
-        space(s.s);
-        word(s.s, constrs_str(cs, ty_constr_to_str));
-      }
       ast::ty_fixed_length(t, v) {
         print_type(s, t);
         word(s.s, ~"/");
@@ -977,9 +971,6 @@ fn print_expr(s: ps, &&expr: @ast::expr) {
       ast::expr_if(test, blk, elseopt) {
         print_if(s, test, blk, elseopt, false);
       }
-      ast::expr_if_check(test, blk, elseopt) {
-        print_if(s, test, blk, elseopt, true);
-      }
       ast::expr_while(test, blk) {
         head(s, ~"while");
         print_maybe_parens_discrim(s, test);
@@ -1131,15 +1122,6 @@ fn print_expr(s: ps, &&expr: @ast::expr) {
           }
         }
       }
-      ast::expr_check(m, expr) {
-        alt m {
-          ast::claimed_expr { word_nbsp(s, ~"claim"); }
-          ast::checked_expr { word_nbsp(s, ~"check"); }
-        }
-        popen(s);
-        print_expr(s, expr);
-        pclose(s);
-      }
       ast::expr_assert(expr) {
         word_nbsp(s, ~"assert");
         print_expr(s, expr);
@@ -1166,7 +1148,7 @@ fn print_expr_parens_if_not_bot(s: ps, ex: @ast::expr) {
       ast::expr_assign_op(_, _, _) | ast::expr_swap(_, _) |
       ast::expr_log(_, _, _) | ast::expr_assert(_) |
       ast::expr_call(_, _, true) |
-      ast::expr_check(_, _) | ast::expr_vstore(_, _) { true }
+      ast::expr_vstore(_, _) { true }
       _ { false }
     };
     if parens { popen(s); }
@@ -1348,9 +1330,6 @@ fn print_fn_args_and_ret(s: ps, decl: ast::fn_decl,
     popen(s);
     print_fn_args(s, decl, cap_items);
     pclose(s);
-    word(s.s, constrs_str(decl.constraints, |c| {
-        ast_fn_constr_to_str(decl, c)
-    }));
 
     maybe_print_comment(s, decl.output.span.lo);
     if decl.output.node != ast::ty_nil {
@@ -1552,7 +1531,6 @@ fn print_ty_fn(s: ps, opt_proto: option<ast::proto>,
         else { print_type(s, decl.output); }
         end(s);
     }
-    word(s.s, constrs_str(decl.constraints, ast_ty_fn_constr_to_str));
     end(s);
 }
 
@@ -1736,67 +1714,6 @@ fn next_comment(s: ps) -> option<comments::cmnt> {
     }
 }
 
-fn constr_args_to_str<T>(f: fn@(T) -> ~str,
-                         args: ~[@ast::sp_constr_arg<T>]) ->
-   ~str {
-    let mut comma = false;
-    let mut s = ~"(";
-    for args.each |a| {
-        if comma { s += ~", "; } else { comma = true; }
-        s += constr_arg_to_str::<T>(f, a.node);
-    }
-    s += ~")";
-    ret s;
-}
-
-fn constr_arg_to_str<T>(f: fn@(T) -> ~str, c: ast::constr_arg_general_<T>) ->
-   ~str {
-    alt c {
-      ast::carg_base { ret ~"*"; }
-      ast::carg_ident(i) { ret f(i); }
-      ast::carg_lit(l) { ret lit_to_str(l); }
-    }
-}
-
-// needed b/c constr_args_to_str needs
-// something that takes an alias
-// (argh)
-fn uint_to_str(&&i: uint) -> ~str { ret uint::str(i); }
-
-fn ast_ty_fn_constr_to_str(&&c: @ast::constr) -> ~str {
-    ret path_to_str(c.node.path) +
-            constr_args_to_str(uint_to_str, c.node.args);
-}
-
-fn ast_fn_constr_to_str(decl: ast::fn_decl, &&c: @ast::constr) -> ~str {
-    let arg_to_str = |a| fn_arg_idx_to_str(decl, a);
-    ret path_to_str(c.node.path) +
-            constr_args_to_str(arg_to_str, c.node.args);
-}
-
-fn ty_constr_to_str(&&c: @ast::ty_constr) -> ~str {
-    fn ty_constr_path_to_str(&&p: @ast::path) -> ~str {
-        ~"*." + path_to_str(p)
-    }
-
-    ret path_to_str(c.node.path) +
-            constr_args_to_str::<@ast::path>(ty_constr_path_to_str,
-                                             c.node.args);
-}
-
-fn constrs_str<T>(constrs: ~[T], elt: fn(T) -> ~str) -> ~str {
-    let mut s = ~"", colon = true;
-    for constrs.each |c| {
-        if colon { s += ~" : "; colon = false; } else { s += ~", "; }
-        s += elt(c);
-    }
-    ret s;
-}
-
-fn fn_arg_idx_to_str(decl: ast::fn_decl, &&idx: uint) -> ~str {
-    *decl.inputs[idx].ident
-}
-
 fn opt_proto_to_str(opt_p: option<ast::proto>) -> ~str {
     alt opt_p {
       none { ~"fn" }
diff --git a/src/libsyntax/visit.rs b/src/libsyntax/visit.rs
index 86ba214f23c..3e61f3706f9 100644
--- a/src/libsyntax/visit.rs
+++ b/src/libsyntax/visit.rs
@@ -44,8 +44,6 @@ fn tps_of_fn(fk: fn_kind) -> ~[ty_param] {
 }
 
 type visitor<E> =
-    // takes the components so that one function can be
-    // generic over constr and ty_constr
     @{visit_mod: fn@(_mod, span, node_id, E, vt<E>),
       visit_view_item: fn@(@view_item, E, vt<E>),
       visit_foreign_item: fn@(@foreign_item, E, vt<E>),
@@ -59,7 +57,6 @@ type visitor<E> =
       visit_expr: fn@(@expr, E, vt<E>),
       visit_ty: fn@(@ty, E, vt<E>),
       visit_ty_params: fn@(~[ty_param], E, vt<E>),
-      visit_constr: fn@(@path, span, node_id, E, vt<E>),
       visit_fn: fn@(fn_kind, fn_decl, blk, span, node_id, E, vt<E>),
       visit_ty_method: fn@(ty_method, E, vt<E>),
       visit_trait_method: fn@(trait_method, E, vt<E>),
@@ -79,7 +76,6 @@ fn default_visitor<E>() -> visitor<E> {
           visit_expr: |a,b,c|visit_expr::<E>(a, b, c),
           visit_ty: |a,b,c|skip_ty::<E>(a, b, c),
           visit_ty_params: |a,b,c|visit_ty_params::<E>(a, b, c),
-          visit_constr: |a,b,c,d,e|visit_constr::<E>(a, b, c, d, e),
           visit_fn: |a,b,c,d,e,f,g|visit_fn::<E>(a, b, c, d, e, f, g),
           visit_ty_method: |a,b,c|visit_ty_method::<E>(a, b, c),
           visit_trait_method: |a,b,c|visit_trait_method::<E>(a, b, c),
@@ -194,21 +190,12 @@ fn visit_ty<E>(t: @ty, e: E, v: vt<E>) {
       ty_tup(ts) { for ts.each |tt| { v.visit_ty(tt, e, v); } }
       ty_fn(_, decl) {
         for decl.inputs.each |a| { v.visit_ty(a.ty, e, v); }
-        for decl.constraints.each |c| {
-            v.visit_constr(c.node.path, c.span, c.node.id, e, v);
-        }
         v.visit_ty(decl.output, e, v);
       }
       ty_path(p, _) { visit_path(p, e, v); }
       ty_fixed_length(t, _) {
         v.visit_ty(t, e, v);
       }
-      ty_constr(t, cs) {
-        v.visit_ty(t, e, v);
-        for cs.each |tc| {
-            v.visit_constr(tc.node.path, tc.span, tc.node.id, e, v);
-        }
-      }
       ty_nil |
       ty_bot |
       ty_mac(_) |
@@ -217,11 +204,6 @@ fn visit_ty<E>(t: @ty, e: E, v: vt<E>) {
     }
 }
 
-fn visit_constr<E>(_operator: @path, _sp: span, _id: node_id, _e: E,
-                   _v: vt<E>) {
-    // default
-}
-
 fn visit_path<E>(p: @path, e: E, v: vt<E>) {
     for p.types.each |tp| { v.visit_ty(tp, e, v); }
 }
@@ -272,9 +254,6 @@ fn visit_ty_params<E>(tps: ~[ty_param], e: E, v: vt<E>) {
 
 fn visit_fn_decl<E>(fd: fn_decl, e: E, v: vt<E>) {
     for fd.inputs.each |a| { v.visit_ty(a.ty, e, v); }
-    for fd.constraints.each |c| {
-        v.visit_constr(c.node.path, c.span, c.node.id, e, v);
-    }
     v.visit_ty(fd.output, e, v);
 }
 
@@ -394,9 +373,7 @@ fn visit_expr<E>(ex: @expr, e: E, v: vt<E>) {
       expr_binary(_, a, b) { v.visit_expr(a, e, v); v.visit_expr(b, e, v); }
       expr_addr_of(_, x) | expr_unary(_, x) |
       expr_loop_body(x) | expr_do_body(x) |
-      expr_check(_, x) | expr_assert(x) {
-        v.visit_expr(x, e, v);
-      }
+      expr_assert(x) { v.visit_expr(x, e, v); }
       expr_lit(_) { }
       expr_cast(x, t) { v.visit_expr(x, e, v); v.visit_ty(t, e, v); }
       expr_if(x, b, eo) {
@@ -404,11 +381,6 @@ fn visit_expr<E>(ex: @expr, e: E, v: vt<E>) {
         v.visit_block(b, e, v);
         visit_expr_opt(eo, e, v);
       }
-      expr_if_check(x, b, eo) {
-        v.visit_expr(x, e, v);
-        v.visit_block(b, e, v);
-        visit_expr_opt(eo, e, v);
-      }
       expr_while(x, b) { v.visit_expr(x, e, v); v.visit_block(b, e, v); }
       expr_loop(b) { v.visit_block(b, e, v); }
       expr_alt(x, arms, _) {
@@ -460,8 +432,6 @@ fn visit_arm<E>(a: arm, e: E, v: vt<E>) {
 // calls the given functions on the nodes.
 
 type simple_visitor =
-    // takes the components so that one function can be
-    // generic over constr and ty_constr
     @{visit_mod: fn@(_mod, span, node_id),
       visit_view_item: fn@(@view_item),
       visit_foreign_item: fn@(@foreign_item),
@@ -475,7 +445,6 @@ type simple_visitor =
       visit_expr: fn@(@expr),
       visit_ty: fn@(@ty),
       visit_ty_params: fn@(~[ty_param]),
-      visit_constr: fn@(@path, span, node_id),
       visit_fn: fn@(fn_kind, fn_decl, blk, span, node_id),
       visit_ty_method: fn@(ty_method),
       visit_trait_method: fn@(trait_method),
@@ -497,7 +466,6 @@ fn default_simple_visitor() -> simple_visitor {
           visit_expr: fn@(_e: @expr) { },
           visit_ty: simple_ignore_ty,
           visit_ty_params: fn@(_ps: ~[ty_param]) {},
-          visit_constr: fn@(_p: @path, _sp: span, _id: node_id) { },
           visit_fn: fn@(_fk: fn_kind, _d: fn_decl, _b: blk, _sp: span,
                         _id: node_id) { },
           visit_ty_method: fn@(_m: ty_method) { },
@@ -572,11 +540,6 @@ fn mk_simple_visitor(v: simple_visitor) -> vt<()> {
         f(ps);
         visit_ty_params(ps, e, v);
     }
-    fn v_constr(f: fn@(@path, span, node_id), pt: @path, sp: span,
-                id: node_id, &&e: (), v: vt<()>) {
-        f(pt, sp, id);
-        visit_constr(pt, sp, id, e, v);
-    }
     fn v_fn(f: fn@(fn_kind, fn_decl, blk, span, node_id),
             fk: fn_kind, decl: fn_decl, body: blk, sp: span,
             id: node_id, &&e: (), v: vt<()>) {
@@ -610,8 +573,6 @@ fn mk_simple_visitor(v: simple_visitor) -> vt<()> {
                 visit_ty: visit_ty,
                 visit_ty_params: |a,b,c|
                     v_ty_params(v.visit_ty_params, a, b, c),
-                visit_constr: |a,b,c,d,e|
-                    v_constr(v.visit_constr, a, b, c, d, e),
                 visit_fn: |a,b,c,d,e,f,g|
                     v_fn(v.visit_fn, a, b, c, d, e, f, g),
                 visit_ty_method: |a,b,c|
diff --git a/src/rustc/back/rpath.rs b/src/rustc/back/rpath.rs
index 7062d6e997e..9f6b703281d 100644
--- a/src/rustc/back/rpath.rs
+++ b/src/rustc/back/rpath.rs
@@ -97,7 +97,6 @@ fn get_rpaths_relative_to_output(os: session::os,
                                  output: path::path,
                                  libs: ~[path::path]) -> ~[~str] {
     vec::map(libs, |a| {
-        check not_win32(os);
         get_rpath_relative_to_output(os, cwd, output, a)
     })
 }
@@ -105,7 +104,9 @@ fn get_rpaths_relative_to_output(os: session::os,
 fn get_rpath_relative_to_output(os: session::os,
                                 cwd: path::path,
                                 output: path::path,
-                                &&lib: path::path) : not_win32(os) -> ~str {
+                                &&lib: path::path) -> ~str {
+    assert not_win32(os);
+
     // Mac doesn't appear to support $ORIGIN
     let prefix = alt os {
         session::os_linux { ~"$ORIGIN" + path::path_sep() }
@@ -147,7 +148,7 @@ fn get_relative_to(abs1: path::path, abs2: path::path) -> path::path {
     // FIXME (#2880): use view here.
     vec::push_all(path, vec::slice(split2, start_idx, len2 - 1u));
 
-    if check vec::is_not_empty(path) {
+    if vec::is_not_empty(path) {
         ret path::connect_many(path);
     } else {
         ret ~".";
@@ -314,18 +315,16 @@ mod test {
     #[test]
     #[cfg(target_os = "linux")]
     fn test_rpath_relative() {
-        let o = session::os_linux;
-        check not_win32(o);
-        let res = get_rpath_relative_to_output(o,
+      let o = session::os_linux;
+      let res = get_rpath_relative_to_output(o,
             ~"/usr", ~"bin/rustc", ~"lib/libstd.so");
-        assert res == ~"$ORIGIN/../lib";
+      assert res == ~"$ORIGIN/../lib";
     }
 
     #[test]
     #[cfg(target_os = "freebsd")]
     fn test_rpath_relative() {
         let o = session::os_freebsd;
-        check not_win32(o);
         let res = get_rpath_relative_to_output(o,
             ~"/usr", ~"bin/rustc", ~"lib/libstd.so");
         assert res == ~"$ORIGIN/../lib";
@@ -336,7 +335,6 @@ mod test {
     fn test_rpath_relative() {
         // this is why refinements would be nice
         let o = session::os_macos;
-        check not_win32(o);
         let res = get_rpath_relative_to_output(o, ~"/usr", ~"bin/rustc",
                                                ~"lib/libstd.so");
         assert res == ~"@executable_path/../lib";
diff --git a/src/rustc/driver/driver.rs b/src/rustc/driver/driver.rs
index 47b126df332..a81b491f23f 100644
--- a/src/rustc/driver/driver.rs
+++ b/src/rustc/driver/driver.rs
@@ -207,9 +207,6 @@ fn compile_upto(sess: session, cfg: ast::crate_cfg,
     let last_use_map = time(time_passes, ~"liveness checking", ||
         middle::liveness::check_crate(ty_cx, method_map, crate));
 
-    time(time_passes, ~"typestate checking", ||
-         middle::tstate::ck::check_crate(ty_cx, crate));
-
     let (root_map, mutbl_map) = time(time_passes, ~"borrow checking", ||
         middle::borrowck::check_crate(ty_cx, method_map,
                                       last_use_map, crate));
diff --git a/src/rustc/front/test.rs b/src/rustc/front/test.rs
index be0d66519dc..2e9b380314a 100644
--- a/src/rustc/front/test.rs
+++ b/src/rustc/front/test.rs
@@ -221,8 +221,7 @@ fn mk_tests(cx: test_ctxt) -> @ast::item {
         {inputs: ~[],
          output: ret_ty,
          purity: ast::impure_fn,
-         cf: ast::return_val,
-         constraints: ~[]};
+         cf: ast::return_val};
 
     // The vector of test_descs for this crate
     let test_descs = mk_test_desc_vec(cx);
@@ -382,8 +381,7 @@ fn mk_test_wrapper(cx: test_ctxt,
         inputs: ~[],
         output: @{id: cx.sess.next_node_id(), node: ast::ty_nil, span: span},
         purity: ast::impure_fn,
-        cf: ast::return_val,
-        constraints: ~[]
+        cf: ast::return_val
     };
 
     let wrapper_body: ast::blk = nospan({
@@ -436,8 +434,7 @@ fn mk_main(cx: test_ctxt) -> @ast::item {
         {inputs: ~[args_arg],
          output: @ret_ty,
          purity: ast::impure_fn,
-         cf: ast::return_val,
-         constraints: ~[]};
+         cf: ast::return_val};
 
     let test_main_call_expr = mk_test_main_call(cx);
 
diff --git a/src/rustc/metadata/tydecode.rs b/src/rustc/metadata/tydecode.rs
index 122a29eb34f..28056838a7a 100644
--- a/src/rustc/metadata/tydecode.rs
+++ b/src/rustc/metadata/tydecode.rs
@@ -63,31 +63,6 @@ fn parse_ret_ty(st: @pstate, conv: conv_did) -> (ast::ret_style, ty::t) {
     }
 }
 
-fn parse_constrs_gen<T: copy>(st: @pstate, conv: conv_did,
-                                       pser: fn(@pstate)
-  -> ast::constr_arg_general_<T>) -> ~[@ty::constr_general<T>] {
-    let mut rslt: ~[@ty::constr_general<T>] = ~[];
-    alt peek(st) {
-      ':' {
-        loop {
-          next(st);
-          vec::push(rslt, parse_constr(st, conv, pser));
-          if peek(st) != ';' { break; }
-        }
-      }
-      _ {}
-    }
-    rslt
-}
-
-fn parse_constrs(st: @pstate, conv: conv_did) -> ~[@ty::constr] {
-    parse_constrs_gen(st, conv, parse_constr_arg)
-}
-
-fn parse_ty_constrs(st: @pstate, conv: conv_did) -> ~[@ty::type_constr] {
-    parse_constrs_gen(st, conv, parse_ty_constr_arg)
-}
-
 fn parse_path(st: @pstate) -> @ast::path {
     let mut idents: ~[ast::ident] = ~[];
     fn is_last(c: char) -> bool { ret c == '(' || c == ':'; }
@@ -106,59 +81,6 @@ fn parse_path(st: @pstate) -> @ast::path {
     };
 }
 
-fn parse_constr_arg(st: @pstate) -> ast::fn_constr_arg {
-    alt peek(st) {
-      '*' { st.pos += 1u; ret ast::carg_base; }
-      c {
-
-        /* how will we disambiguate between
-           an arg index and a lit argument? */
-        if c >= '0' && c <= '9' {
-            next(st);
-            // FIXME #877
-            ret ast::carg_ident((c as uint) - 48u);
-        } else {
-            #error("Lit args are unimplemented");
-            fail; // FIXME #877
-        }
-        /*
-          else {
-          auto lit = parse_lit(st, conv, ',');
-          vec::push(args, respan(st.span, ast::carg_lit(lit)));
-          }
-        */
-      }
-    }
-}
-
-fn parse_ty_constr_arg(st: @pstate) -> ast::constr_arg_general_<@path> {
-    alt peek(st) {
-      '*' { st.pos += 1u; ret ast::carg_base; }
-      c { ret ast::carg_ident(parse_path(st)); }
-    }
-}
-
-fn parse_constr<T: copy>(st: @pstate, conv: conv_did,
-                         pser: fn(@pstate) -> ast::constr_arg_general_<T>)
-    -> @ty::constr_general<T> {
-    // FIXME: use real spans and not a bogus one (#2407)
-    let sp = ast_util::dummy_sp();
-    let mut args: ~[@sp_constr_arg<T>] = ~[];
-    let pth = parse_path(st);
-    let mut ignore: char = next(st);
-    assert (ignore == '(');
-    let def = parse_def(st, conv);
-    let mut an_arg: constr_arg_general_<T>;
-    loop {
-        an_arg = pser(st);
-        vec::push(args, @respan(sp, an_arg));
-        ignore = next(st);
-        if ignore != ';' { break; }
-    }
-    assert (ignore == ')');
-    ret @respan(sp, {path: pth, args: args, id: def});
-}
-
 fn parse_ty_rust_fn(st: @pstate, conv: conv_did) -> ty::t {
     ret ty::mk_fn(st.tcx, parse_ty_fn(st, conv));
 }
@@ -363,13 +285,6 @@ fn parse_ty(st: @pstate, conv: conv_did) -> ty::t {
           }
         }
       }
-      'A' {
-        assert (next(st) == '[');
-        let tt = parse_ty(st, conv);
-        let tcs = parse_ty_constrs(st, conv);
-        assert (next(st) == ']');
-        ret ty::mk_constr(st.tcx, tt, tcs);
-      }
       '"' {
         let def = parse_def(st, conv);
         let inner = parse_ty(st, conv);
@@ -457,10 +372,9 @@ fn parse_ty_fn(st: @pstate, conv: conv_did) -> ty::fn_ty {
         vec::push(inputs, {mode: ast::expl(mode), ty: parse_ty(st, conv)});
     }
     st.pos += 1u; // eat the ']'
-    let cs = parse_constrs(st, conv);
     let (ret_style, ret_ty) = parse_ret_ty(st, conv);
     ret {purity: purity, proto: proto, inputs: inputs, output: ret_ty,
-         ret_style: ret_style, constraints: cs};
+         ret_style: ret_style};
 }
 
 
diff --git a/src/rustc/metadata/tyencode.rs b/src/rustc/metadata/tyencode.rs
index cb8881fdf2a..9a6ddaf7c59 100644
--- a/src/rustc/metadata/tyencode.rs
+++ b/src/rustc/metadata/tyencode.rs
@@ -285,12 +285,6 @@ fn enc_sty(w: io::writer, cx: @ctxt, st: ty::sty) {
       ty::ty_opaque_closure_ptr(ty::ck_block) { w.write_str(&"C&"); }
       ty::ty_opaque_closure_ptr(ty::ck_box) { w.write_str(&"C@"); }
       ty::ty_opaque_closure_ptr(ty::ck_uniq) { w.write_str(&"C~"); }
-      ty::ty_constr(ty, cs) {
-        w.write_str(&"A[");
-        enc_ty(w, cx, ty);
-        for cs.each |tc| { enc_ty_constr(w, cx, tc); }
-        w.write_char(']');
-      }
       ty::ty_opaque_box { w.write_char('B'); }
       ty::ty_class(def, substs) {
           #debug("~~~~ %s", ~"a[");
@@ -344,55 +338,12 @@ fn enc_ty_fn(w: io::writer, cx: @ctxt, ft: ty::fn_ty) {
         enc_ty(w, cx, arg.ty);
     }
     w.write_char(']');
-    let mut colon = true;
-    for ft.constraints.each |c| {
-        if colon {
-            w.write_char(':');
-            colon = false;
-        } else { w.write_char(';'); }
-        enc_constr(w, cx, c);
-    }
     alt ft.ret_style {
       noreturn { w.write_char('!'); }
       _ { enc_ty(w, cx, ft.output); }
     }
 }
 
-fn enc_constr_gen<T>(w: io::writer, cx: @ctxt,
-                  c: @ty::constr_general<T>,
-                  write_arg: fn(@sp_constr_arg<T>)) {
-    w.write_str(path_to_str(c.node.path));
-    w.write_char('(');
-    w.write_str(cx.ds(c.node.id));
-    w.write_char('|');
-    let mut semi = false;
-    for c.node.args.each |a| {
-        if semi { w.write_char(';'); } else { semi = true; }
-        write_arg(a);
-    }
-    w.write_char(')');
-}
-
-fn enc_constr(w: io::writer, cx: @ctxt, c: @ty::constr) {
-    enc_constr_gen(w, cx, c, |a| {
-      alt a.node {
-        carg_base     { w.write_char('*'); }
-        carg_ident(i) { w.write_uint(i); }
-        carg_lit(l)   { w.write_str(lit_to_str(l)); }
-      }
-    });
-}
-
-fn enc_ty_constr(w: io::writer, cx: @ctxt, c: @ty::type_constr) {
-    enc_constr_gen(w, cx, c, |a| {
-      alt a.node {
-        carg_base     { w.write_char('*'); }
-        carg_ident(p) { w.write_str(path_to_str(p)); }
-        carg_lit(l)  { w.write_str(lit_to_str(l)); }
-      }
-    });
-}
-
 fn enc_bounds(w: io::writer, cx: @ctxt, bs: @~[ty::param_bound]) {
     for vec::each(*bs) |bound| {
         alt bound {
diff --git a/src/rustc/middle/borrowck/categorization.rs b/src/rustc/middle/borrowck/categorization.rs
index e0b6d10ca36..e7976cac2e6 100644
--- a/src/rustc/middle/borrowck/categorization.rs
+++ b/src/rustc/middle/borrowck/categorization.rs
@@ -167,11 +167,11 @@ impl public_methods for borrowck_ctxt {
           ast::expr_addr_of(*) | ast::expr_call(*) |
           ast::expr_swap(*) | ast::expr_move(*) | ast::expr_assign(*) |
           ast::expr_assign_op(*) | ast::expr_fn(*) | ast::expr_fn_block(*) |
-          ast::expr_assert(*) | ast::expr_check(*) | ast::expr_ret(*) |
+          ast::expr_assert(*) | ast::expr_ret(*) |
           ast::expr_loop_body(*) | ast::expr_do_body(*) | ast::expr_unary(*) |
           ast::expr_copy(*) | ast::expr_cast(*) | ast::expr_fail(*) |
           ast::expr_vstore(*) | ast::expr_vec(*) | ast::expr_tup(*) |
-          ast::expr_if_check(*) | ast::expr_if(*) | ast::expr_log(*) |
+          ast::expr_if(*) | ast::expr_log(*) |
           ast::expr_new(*) | ast::expr_binary(*) | ast::expr_while(*) |
           ast::expr_block(*) | ast::expr_loop(*) | ast::expr_alt(*) |
           ast::expr_lit(*) | ast::expr_break | ast::expr_mac(*) |
diff --git a/src/rustc/middle/liveness.rs b/src/rustc/middle/liveness.rs
index 6bce1ab88d1..02d24772c25 100644
--- a/src/rustc/middle/liveness.rs
+++ b/src/rustc/middle/liveness.rs
@@ -453,8 +453,7 @@ fn visit_expr(expr: @expr, &&self: @ir_maps, vt: vt<@ir_maps>) {
       }
 
       // live nodes required for interesting control flow:
-      expr_if_check(*) | expr_if(*) | expr_alt(*) |
-      expr_while(*) | expr_loop(*) {
+      expr_if(*) | expr_alt(*) | expr_while(*) | expr_loop(*) {
         (*self).add_live_node_for_node(expr.id, lnk_expr(expr.span));
         visit::visit_expr(expr, self, vt);
       }
@@ -467,7 +466,7 @@ fn visit_expr(expr: @expr, &&self: @ir_maps, vt: vt<@ir_maps>) {
       expr_index(*) | expr_field(*) | expr_vstore(*) |
       expr_vec(*) | expr_rec(*) | expr_call(*) | expr_tup(*) |
       expr_new(*) | expr_log(*) | expr_binary(*) |
-      expr_assert(*) | expr_check(*) | expr_addr_of(*) | expr_copy(*) |
+      expr_assert(*) | expr_addr_of(*) | expr_copy(*) |
       expr_loop_body(*) | expr_do_body(*) | expr_cast(*) |
       expr_unary(*) | expr_fail(*) |
       expr_break | expr_again | expr_lit(_) | expr_ret(*) |
@@ -936,7 +935,6 @@ class liveness {
             }
           }
 
-          expr_if_check(cond, then, els) |
           expr_if(cond, then, els) {
             //
             //     (cond)
@@ -1098,7 +1096,6 @@ class liveness {
           }
 
           expr_assert(e) |
-          expr_check(_, e) |
           expr_addr_of(_, e) |
           expr_copy(e) |
           expr_loop_body(e) |
@@ -1449,12 +1446,12 @@ fn check_expr(expr: @expr, &&self: @liveness, vt: vt<@liveness>) {
       }
 
       // no correctness conditions related to liveness
-      expr_if_check(*) | expr_if(*) | expr_alt(*) |
+      expr_if(*) | expr_alt(*) |
       expr_while(*) | expr_loop(*) |
       expr_index(*) | expr_field(*) | expr_vstore(*) |
       expr_vec(*) | expr_rec(*) | expr_tup(*) |
       expr_new(*) | expr_log(*) | expr_binary(*) |
-      expr_assert(*) | expr_check(*) | expr_copy(*) |
+      expr_assert(*) | expr_copy(*) |
       expr_loop_body(*) | expr_do_body(*) |
       expr_cast(*) | expr_unary(*) | expr_fail(*) |
       expr_ret(*) | expr_break | expr_again | expr_lit(_) |
diff --git a/src/rustc/middle/resolve.rs b/src/rustc/middle/resolve.rs
index 9d026b1cc20..a4c85bee55e 100644
--- a/src/rustc/middle/resolve.rs
+++ b/src/rustc/middle/resolve.rs
@@ -428,7 +428,6 @@ fn resolve_names(e: @env, c: @ast::crate) {
           visit_expr: |a,b,c| walk_expr(e, a, b ,c),
           visit_ty: |a,b,c| walk_ty(e, a, b, c),
           visit_ty_params: |a,b,c| walk_tps(e, a, b, c),
-          visit_constr: |a,b,c,d,f| walk_constr(e, a, b, c, d, f),
           visit_fn: |a,b,c,d,f,g,h| {
               visit_fn_with_scope(e, a, b, c, d, f, g, h)
           }
@@ -662,7 +661,6 @@ fn visit_fn_with_scope(e: @env, fk: visit::fn_kind, decl: ast::fn_decl,
 
     // here's where we need to set up the mapping
     // for f's constrs in the table.
-    for decl.constraints.each |c| { resolve_constr(e, c, sc, v); }
     let scope = alt fk {
       visit::fk_item_fn(_, tps) | visit::fk_method(_, tps, _)
       | visit::fk_ctor(_, tps, _, _) | visit::fk_dtor(tps, _, _) {
@@ -767,19 +765,6 @@ fn follow_import(e: env, &&sc: scopes, path: ~[ident], sp: span) ->
     } else { ret none; }
 }
 
-fn resolve_constr(e: @env, c: @ast::constr, &&sc: scopes, _v: vt<scopes>) {
-    alt lookup_path_strict(*e, sc, c.span, c.node.path, ns_val) {
-       some(d@ast::def_fn(_,ast::pure_fn)) {
-         e.def_map.insert(c.node.id, d);
-       }
-       _ {
-           let s = path_to_str(c.node.path);
-           e.sess.span_err(c.span, #fmt("%s is not declared pure. Try \
-             `pure fn %s` instead of `fn %s`.", s, s, s));
-       }
-    }
-}
-
 // Import resolution
 fn resolve_import(e: env, n_id: node_id, name: ast::ident,
                   ids: ~[ast::ident], sp: codemap::span, &&sc: scopes) {
diff --git a/src/rustc/middle/resolve3.rs b/src/rustc/middle/resolve3.rs
index 07af1e5538a..9e742f38bac 100644
--- a/src/rustc/middle/resolve3.rs
+++ b/src/rustc/middle/resolve3.rs
@@ -20,7 +20,7 @@ import syntax::ast::{item_ty, local, local_crate, method, node_id, pat};
 import syntax::ast::{pat_enum, pat_ident, path, prim_ty, stmt_decl, ty,
                      pat_box, pat_uniq, pat_lit, pat_range, pat_rec,
                      pat_tup, pat_wild};
-import syntax::ast::{ty_bool, ty_char, ty_constr, ty_f, ty_f32, ty_f64};
+import syntax::ast::{ty_bool, ty_char, ty_f, ty_f32, ty_f64};
 import syntax::ast::{ty_float, ty_i, ty_i16, ty_i32, ty_i64, ty_i8, ty_int};
 import syntax::ast::{ty_param, ty_path, ty_str, ty_u, ty_u16, ty_u32, ty_u64};
 import syntax::ast::{ty_u8, ty_uint, variant, view_item, view_item_export};
@@ -3163,21 +3163,6 @@ class Resolver {
                     }
 
                     self.resolve_type(declaration.output, visitor);
-
-                    // Resolve constraints.
-                    for declaration.constraints.each |constraint| {
-                        alt self.resolve_path(constraint.node.path, ValueNS,
-                                              false, visitor) {
-                            none {
-                                self.session.span_err(constraint.span,
-                                    #fmt("unresolved name: %s",
-                                    *constraint.node.path.idents.last()));
-                            }
-                            some(def) {
-                                self.record_def(constraint.node.id, def);
-                            }
-                        }
-                    }
                 }
             }
 
@@ -3560,25 +3545,6 @@ class Resolver {
                 }
             }
 
-            ty_constr(base_type, constraints) {
-                self.resolve_type(base_type, visitor);
-
-                for constraints.each |constraint| {
-                    alt self.resolve_path(constraint.node.path, ValueNS,
-                                          false, visitor) {
-                        none {
-                            self.session.span_err(constraint.span,
-                                                  ~"(resolving function) \
-                                                   use of undeclared \
-                                                   constraint");
-                        }
-                        some(def) {
-                            self.record_def(constraint.node.id, def);
-                        }
-                    }
-                }
-            }
-
             _ {
                 // Just resolve embedded types.
                 visit_ty(ty, (), visitor);
diff --git a/src/rustc/middle/trans/base.rs b/src/rustc/middle/trans/base.rs
index 02b3733eaf7..212ba14a516 100644
--- a/src/rustc/middle/trans/base.rs
+++ b/src/rustc/middle/trans/base.rs
@@ -2002,19 +2002,23 @@ fn trans_external_path(ccx: @crate_ctxt, did: ast::def_id, t: ty::t)
 fn normalize_for_monomorphization(tcx: ty::ctxt, ty: ty::t) -> option<ty::t> {
     // FIXME[mono] could do this recursively. is that worthwhile? (#2529)
     alt ty::get(ty).struct {
-      ty::ty_box(mt) { some(ty::mk_opaque_box(tcx)) }
-      ty::ty_fn(fty) { some(ty::mk_fn(tcx, {purity: ast::impure_fn,
-                                            proto: fty.proto,
-                                            inputs: ~[],
-                                            output: ty::mk_nil(tcx),
-                                            ret_style: ast::return_val,
-                                            constraints: ~[]})) }
-      ty::ty_trait(_, _) { some(ty::mk_fn(tcx, {purity: ast::impure_fn,
-                                                proto: ast::proto_box,
-                                                inputs: ~[],
-                                                output: ty::mk_nil(tcx),
-                                                ret_style: ast::return_val,
-                                                constraints: ~[]})) }
+      ty::ty_box(mt) {
+        some(ty::mk_opaque_box(tcx))
+      }
+      ty::ty_fn(fty) {
+        some(ty::mk_fn(tcx, {purity: ast::impure_fn,
+                             proto: fty.proto,
+                             inputs: ~[],
+                             output: ty::mk_nil(tcx),
+                             ret_style: ast::return_val}))
+      }
+      ty::ty_trait(_, _) {
+        some(ty::mk_fn(tcx, {purity: ast::impure_fn,
+                             proto: ast::proto_box,
+                             inputs: ~[],
+                             output: ty::mk_nil(tcx),
+                             ret_style: ast::return_val}))
+      }
       ty::ty_ptr(_) { some(ty::mk_uint(tcx)) }
       _ { none }
     }
@@ -3525,7 +3529,7 @@ fn trans_expr(bcx: block, e: @ast::expr, dest: dest) -> block {
     fn unrooted(bcx: block, e: @ast::expr, dest: dest) -> block {
         let tcx = bcx.tcx();
         alt e.node {
-          ast::expr_if(cond, thn, els) | ast::expr_if_check(cond, thn, els) {
+          ast::expr_if(cond, thn, els) {
             ret trans_if(bcx, cond, thn, els, dest);
           }
           ast::expr_alt(expr, arms, mode) {
@@ -3631,23 +3635,6 @@ fn trans_expr(bcx: block, e: @ast::expr, dest: dest) -> block {
             assert dest == ignore;
             ret trans_check_expr(bcx, e, a, ~"Assertion");
           }
-          ast::expr_check(ast::checked_expr, a) {
-            assert dest == ignore;
-            ret trans_check_expr(bcx, e, a, ~"Predicate");
-          }
-          ast::expr_check(ast::claimed_expr, a) {
-            assert dest == ignore;
-            /* Claims are turned on and off by a global variable
-            that the RTS sets. This case generates code to
-            check the value of that variable, doing nothing
-            if it's set to false and acting like a check
-            otherwise. */
-            let c = get_extern_const(bcx.ccx().externs, bcx.ccx().llmod,
-                                     ~"check_claims", T_bool());
-            ret do with_cond(bcx, Load(bcx, c)) |bcx| {
-                trans_check_expr(bcx, e, a, ~"Claim")
-            };
-          }
           ast::expr_while(cond, body) {
             assert dest == ignore;
             ret trans_while(bcx, cond, body);
diff --git a/src/rustc/middle/trans/foreign.rs b/src/rustc/middle/trans/foreign.rs
index 847aca0db2c..fca21eb3a8e 100644
--- a/src/rustc/middle/trans/foreign.rs
+++ b/src/rustc/middle/trans/foreign.rs
@@ -976,8 +976,7 @@ fn trans_intrinsic(ccx: @crate_ctxt, decl: ValueRef, item: @ast::foreign_item,
                     ty::mk_mach_uint(bcx.tcx(), ast::ty_u8))
             }],
             output: ty::mk_nil(bcx.tcx()),
-            ret_style: ast::return_val,
-            constraints: ~[]
+            ret_style: ast::return_val
         });
         bcx = trans_call_inner(bcx, none, fty, ty::mk_nil(bcx.tcx()),
                                |bcx| lval_no_env(
diff --git a/src/rustc/middle/trans/reflect.rs b/src/rustc/middle/trans/reflect.rs
index d71151316a1..6ce5f2f387d 100644
--- a/src/rustc/middle/trans/reflect.rs
+++ b/src/rustc/middle/trans/reflect.rs
@@ -276,7 +276,6 @@ impl methods for reflector {
           ty::ty_self { self.leaf(~"self") }
           ty::ty_type { self.leaf(~"type") }
           ty::ty_opaque_box { self.leaf(~"opaque_box") }
-          ty::ty_constr(t, _) { self.visit(~"constr", ~[self.c_tydesc(t)]) }
           ty::ty_opaque_closure_ptr(ck) {
             let ckval = alt ck {
               ty::ck_block { 0u }
diff --git a/src/rustc/middle/trans/shape.rs b/src/rustc/middle/trans/shape.rs
index 801c642570c..71a15b7f05e 100644
--- a/src/rustc/middle/trans/shape.rs
+++ b/src/rustc/middle/trans/shape.rs
@@ -357,7 +357,6 @@ fn shape_of(ccx: @crate_ctxt, t: ty::t) -> ~[u8] {
       ty::ty_fn({proto: ast::proto_any, _}) { ~[shape_stack_fn] }
       ty::ty_fn({proto: ast::proto_bare, _}) { ~[shape_bare_fn] }
       ty::ty_opaque_closure_ptr(_) { ~[shape_opaque_closure_ptr] }
-      ty::ty_constr(inner_t, _) { shape_of(ccx, inner_t) }
       ty::ty_var(_) | ty::ty_var_integral(_) | ty::ty_self {
         ccx.sess.bug(~"shape_of: unexpected type struct found");
       }
diff --git a/src/rustc/middle/trans/type_of.rs b/src/rustc/middle/trans/type_of.rs
index dc122034709..ab3384dad25 100644
--- a/src/rustc/middle/trans/type_of.rs
+++ b/src/rustc/middle/trans/type_of.rs
@@ -148,7 +148,6 @@ fn type_of(cx: @crate_ctxt, t: ty::t) -> TypeRef {
             T_struct(tys)
           }
           ty::ty_opaque_closure_ptr(_) { T_opaque_box_ptr(cx) }
-          ty::ty_constr(subt,_) { type_of(cx, subt) }
           ty::ty_class(*) {
             // Only create the named struct, but don't fill it in. We fill it
             // in *after* placing it into the type cache. This prevents
diff --git a/src/rustc/middle/trans/type_use.rs b/src/rustc/middle/trans/type_use.rs
index 8d741655d35..95dfffff07e 100644
--- a/src/rustc/middle/trans/type_use.rs
+++ b/src/rustc/middle/trans/type_use.rs
@@ -243,8 +243,8 @@ fn mark_for_expr(cx: ctx, e: @expr) {
       }
       expr_alt(_, _, _) | expr_block(_) | expr_if(_, _, _) |
       expr_while(_, _) | expr_fail(_) | expr_break | expr_again |
-      expr_unary(_, _) | expr_lit(_) | expr_assert(_) | expr_check(_, _) |
-      expr_if_check(_, _, _) | expr_mac(_) | expr_addr_of(_, _) |
+      expr_unary(_, _) | expr_lit(_) | expr_assert(_) |
+      expr_mac(_) | expr_addr_of(_, _) |
       expr_ret(_) | expr_loop(_) |
       expr_loop_body(_) | expr_do_body(_) {}
     }
diff --git a/src/rustc/middle/tstate/bitvectors.rs b/src/rustc/middle/tstate/bitvectors.rs
deleted file mode 100644
index 83151d8627a..00000000000
--- a/src/rustc/middle/tstate/bitvectors.rs
+++ /dev/null
@@ -1,186 +0,0 @@
-import syntax::ast::*;
-import syntax::visit;
-import option::*;
-import aux::*;
-import tstate::ann::{pre_and_post, precond, postcond, prestate, poststate,
-                     relax_prestate, relax_precond, relax_poststate,
-                     pps_len, true_precond,
-                     difference, union, clone,
-                     set_in_postcond, set_in_poststate, set_in_poststate_,
-                     clear_in_poststate, clear_in_prestate,
-                     clear_in_poststate_};
-import tritv::*;
-import driver::session::session;
-import std::map::hashmap;
-
-fn bit_num(fcx: fn_ctxt, c: tsconstr) -> uint {
-    let d = c.def_id;
-    assert (fcx.enclosing.constrs.contains_key(d));
-    let rslt = fcx.enclosing.constrs.get(d);
-    match_args(fcx, rslt.descs, c.args)
-}
-
-fn promises(fcx: fn_ctxt, p: poststate, c: tsconstr) -> bool {
-    ret promises_(bit_num(fcx, c), p);
-}
-
-fn promises_(n: uint, p: poststate) -> bool {
-    ret tritv_get(p, n) == ttrue;
-}
-
-// v "happens after" u
-fn seq_trit(u: trit, v: trit) -> trit {
-    alt v { ttrue { ttrue } tfalse { tfalse } dont_care { u } }
-}
-
-// idea: q "happens after" p -- so if something is
-// 1 in q and 0 in p, it's 1 in the result; however,
-// if it's 0 in q and 1 in p, it's 0 in the result
-fn seq_tritv(p: postcond, q: postcond) {
-    let mut i = 0u;
-    assert (p.nbits == q.nbits);
-    while i < p.nbits {
-        tritv_set(i, p, seq_trit(tritv_get(p, i), tritv_get(q, i)));
-        i += 1u;
-    }
-}
-
-fn seq_postconds(fcx: fn_ctxt, ps: ~[postcond]) -> postcond {
-    let sz = vec::len(ps);
-    if sz >= 1u {
-        let prev = tritv_clone(ps[0]);
-        vec::iter_between(ps, 1u, sz, |p| seq_tritv(prev, p) );
-        ret prev;
-    } else { ret ann::empty_poststate(num_constraints(fcx.enclosing)); }
-}
-
-// Given a list of pres and posts for exprs e0 ... en,
-// return the precondition for evaluating each expr in order.
-// So, if e0's post is {x} and e1's pre is {x, y, z}, the entire
-// precondition shouldn't include x.
-fn seq_preconds(fcx: fn_ctxt, pps: ~[pre_and_post]) -> precond {
-    let sz: uint = vec::len(pps);
-    let num_vars: uint = num_constraints(fcx.enclosing);
-
-    fn seq_preconds_go(fcx: fn_ctxt, pps: ~[pre_and_post],
-                       idx: uint, first: pre_and_post)
-       -> precond {
-        let mut idx = idx;
-        let mut first = first;
-        loop {
-            let sz: uint = vec::len(pps) - idx;
-            if sz >= 1u {
-                let second = pps[0];
-                assert (pps_len(second) == num_constraints(fcx.enclosing));
-                let second_pre = clone(second.precondition);
-                difference(second_pre, first.postcondition);
-                let next_first = clone(first.precondition);
-                union(next_first, second_pre);
-                let next_first_post = clone(first.postcondition);
-                seq_tritv(next_first_post, second.postcondition);
-                idx += 1u;
-                first = {precondition: next_first,
-                         postcondition: next_first_post};
-            } else { ret first.precondition; }
-        }
-    }
-
-    if sz >= 1u {
-        let first = pps[0];
-        assert (pps_len(first) == num_vars);
-        ret seq_preconds_go(fcx, pps, 1u, first);
-    } else { ret true_precond(num_vars); }
-}
-
-fn intersect_states(p: prestate, q: prestate) -> prestate {
-    let rslt = tritv_clone(p);
-    tritv_intersect(rslt, q);
-    ret rslt;
-}
-
-fn gen(fcx: fn_ctxt, id: node_id, c: tsconstr) -> bool {
-    ret set_in_postcond(bit_num(fcx, c),
-                        node_id_to_ts_ann(fcx.ccx, id).conditions);
-}
-
-fn declare_var(fcx: fn_ctxt, c: tsconstr, pre: prestate) -> prestate {
-    let rslt = clone(pre);
-    relax_prestate(bit_num(fcx, c), rslt);
-    // idea is this is scoped
-    relax_poststate(bit_num(fcx, c), rslt);
-    ret rslt;
-}
-
-fn relax_precond_expr(e: @expr, cx: relax_ctxt, vt: visit::vt<relax_ctxt>) {
-    relax_precond(cx.i as uint, expr_precond(cx.fcx.ccx, e));
-    visit::visit_expr(e, cx, vt);
-}
-
-fn relax_precond_stmt(s: @stmt, cx: relax_ctxt, vt: visit::vt<relax_ctxt>) {
-    relax_precond(cx.i as uint, stmt_precond(cx.fcx.ccx, *s));
-    visit::visit_stmt(s, cx, vt);
-}
-
-type relax_ctxt = {fcx: fn_ctxt, i: node_id};
-
-fn relax_precond_block_inner(b: blk, cx: relax_ctxt,
-                             vt: visit::vt<relax_ctxt>) {
-    relax_precond(cx.i as uint, block_precond(cx.fcx.ccx, b));
-    visit::visit_block(b, cx, vt);
-}
-
-fn relax_precond_block(fcx: fn_ctxt, i: node_id, b: blk) {
-    let cx = {fcx: fcx, i: i};
-    let visitor = visit::default_visitor::<relax_ctxt>();
-    let visitor =
-        @{visit_block: relax_precond_block_inner,
-          visit_expr: relax_precond_expr,
-          visit_stmt: relax_precond_stmt,
-          visit_item:
-              fn@(_i: @item, _cx: relax_ctxt, _vt: visit::vt<relax_ctxt>) { },
-          visit_fn: do_nothing
-             with *visitor};
-    let v1 = visit::mk_vt(visitor);
-    v1.visit_block(b, cx, v1);
-}
-
-fn gen_poststate(fcx: fn_ctxt, id: node_id, c: tsconstr) -> bool {
-    #debug("gen_poststate");
-    ret set_in_poststate(bit_num(fcx, c),
-                         node_id_to_ts_ann(fcx.ccx, id).states);
-}
-
-fn kill_prestate(fcx: fn_ctxt, id: node_id, c: tsconstr) -> bool {
-    ret clear_in_prestate(bit_num(fcx, c),
-                          node_id_to_ts_ann(fcx.ccx, id).states);
-}
-
-fn kill_all_prestate(fcx: fn_ctxt, id: node_id) {
-    tritv::tritv_kill(node_id_to_ts_ann(fcx.ccx, id).states.prestate);
-}
-
-
-fn kill_poststate(fcx: fn_ctxt, id: node_id, c: tsconstr) -> bool {
-    #debug("kill_poststate");
-    ret clear_in_poststate(bit_num(fcx, c),
-                           node_id_to_ts_ann(fcx.ccx, id).states);
-}
-
-fn kill_poststate_(fcx: fn_ctxt, c: tsconstr, post: poststate) -> bool {
-    #debug("kill_poststate_");
-    ret clear_in_poststate_(bit_num(fcx, c), post);
-}
-
-fn set_in_prestate_constr(fcx: fn_ctxt, c: tsconstr, t: prestate) -> bool {
-    ret set_in_poststate_(bit_num(fcx, c), t);
-}
-
-//
-// Local Variables:
-// mode: rust
-// fill-column: 78;
-// indent-tabs-mode: nil
-// c-basic-offset: 4
-// buffer-file-coding-system: utf-8-unix
-// End:
-//
diff --git a/src/rustc/middle/ty.rs b/src/rustc/middle/ty.rs
index badfee1fd1c..0e724321b3e 100644
--- a/src/rustc/middle/ty.rs
+++ b/src/rustc/middle/ty.rs
@@ -15,7 +15,7 @@ import middle::lint::{get_warning_level, vecs_not_implicitly_copyable,
                       ignore};
 import syntax::ast::*;
 import syntax::print::pprust::*;
-import util::ppaux::{ty_to_str, tys_to_str, ty_constr_to_str};
+import util::ppaux::{ty_to_str, tys_to_str};
 
 export tv_vid, tvi_vid, region_vid, vid;
 export br_hashmap;
@@ -24,12 +24,8 @@ export node_id_to_type;
 export node_id_to_type_params;
 export arg;
 export args_eq;
-export ast_constr_to_constr;
 export block_ty;
 export class_items_as_fields, class_items_as_mutable_fields;
-export constr;
-export constr_general;
-export constr_table;
 export ctxt;
 export deref, deref_sty;
 export index, index_sty;
@@ -76,10 +72,8 @@ export ty_param_bounds_and_ty;
 export ty_bool, mk_bool, type_is_bool;
 export ty_bot, mk_bot, type_is_bot;
 export ty_box, mk_box, mk_imm_box, type_is_box, type_is_boxed;
-export ty_constr, mk_constr;
 export ty_opaque_closure_ptr, mk_opaque_closure_ptr;
 export ty_opaque_box, mk_opaque_box;
-export ty_constr_arg;
 export ty_float, mk_float, mk_mach_float, type_is_fp;
 export ty_fn, fn_ty, mk_fn;
 export ty_fn_proto, ty_fn_ret, ty_fn_ret_style, tys_in_fn_ty;
@@ -113,7 +107,6 @@ export tbox_has_flag;
 export ty_var_id;
 export ty_to_def_id;
 export ty_fn_args;
-export type_constr;
 export kind, kind_implicitly_copyable, kind_sendable, kind_copyable;
 export kind_noncopyable, kind_const;
 export kind_can_be_copied, kind_can_be_sent, kind_can_be_implicitly_copied;
@@ -168,7 +161,7 @@ export terr_no_integral_type, terr_ty_param_size, terr_self_substs;
 export terr_in_field, terr_record_fields, terr_vstores_differ, terr_arg_count;
 export terr_sorts, terr_vec, terr_str, terr_record_size, terr_tuple_size;
 export terr_regions_differ, terr_mutability, terr_purity_mismatch;
-export terr_constr_mismatch, terr_constr_len, terr_proto_mismatch;
+export terr_proto_mismatch;
 export terr_ret_style_mismatch;
 
 // Data types
@@ -187,8 +180,6 @@ type method = {ident: ast::ident,
                purity: ast::purity,
                vis: ast::visibility};
 
-type constr_table = hashmap<ast::node_id, ~[constr]>;
-
 type mt = {ty: t, mutbl: ast::mutability};
 
 enum vstore {
@@ -316,8 +307,7 @@ type fn_ty = {purity: ast::purity,
               proto: ast::proto,
               inputs: ~[arg],
               output: t,
-              ret_style: ret_style,
-              constraints: ~[@constr]};
+              ret_style: ret_style};
 
 // See discussion at head of region.rs
 enum region {
@@ -379,7 +369,6 @@ enum sty {
                               // integral types only
     ty_param(uint, def_id), // type parameter
     ty_self, // special, implicit `self` type parameter
-    ty_constr(t, ~[@type_constr]),
 
     // "Fake" types, used for trans purposes
     ty_type, // type_desc*
@@ -388,12 +377,6 @@ enum sty {
     ty_unboxed_vec(mt),
 }
 
-// In the middle end, constraints have a def_id attached, referring
-// to the definition of the operator in the constraint.
-type constr_general<ARG> = spanned<constr_general_<ARG, def_id>>;
-type type_constr = constr_general<@path>;
-type constr = constr_general<uint>;
-
 enum terr_vstore_kind {
     terr_vec, terr_str
 }
@@ -416,8 +399,6 @@ enum type_err {
     terr_record_fields(ast::ident, ast::ident),
     terr_arg_count,
     terr_mode_mismatch(mode, mode),
-    terr_constr_len(uint, uint),
-    terr_constr_mismatch(@type_constr, @type_constr),
     terr_regions_differ(region, region),
     terr_vstores_differ(terr_vstore_kind, vstore, vstore),
     terr_in_field(@type_err, ast::ident),
@@ -607,9 +588,6 @@ fn mk_t_with_id(cx: ctxt, st: sty, o_def_id: option<ast::def_id>) -> t {
         for f.inputs.each |a| { flags |= get(a.ty).flags; }
         flags |= get(f.output).flags;
       }
-      ty_constr(tt, _) {
-        flags |= get(tt).flags;
-      }
     }
     let t = @{struct: st, id: cx.next_id, flags: flags, o_def_id: o_def_id};
     cx.interner.insert(key, t);
@@ -700,10 +678,6 @@ fn mk_mut_unboxed_vec(cx: ctxt, ty: t) -> t {
 
 fn mk_rec(cx: ctxt, fs: ~[field]) -> t { mk_t(cx, ty_rec(fs)) }
 
-fn mk_constr(cx: ctxt, t: t, cs: ~[@type_constr]) -> t {
-    mk_t(cx, ty_constr(t, cs))
-}
-
 fn mk_tup(cx: ctxt, ts: ~[t]) -> t { mk_t(cx, ty_tup(ts)) }
 
 fn mk_fn(cx: ctxt, fty: fn_ty) -> t { mk_t(cx, ty_fn(fty)) }
@@ -790,7 +764,6 @@ fn maybe_walk_ty(ty: t, f: fn(t) -> bool) {
         for ft.inputs.each |a| { maybe_walk_ty(a.ty, f); }
         maybe_walk_ty(ft.output, f);
       }
-      ty_constr(sub, _) { maybe_walk_ty(sub, f); }
       ty_uniq(tm) { maybe_walk_ty(tm.ty, f); }
     }
 }
@@ -851,9 +824,6 @@ fn fold_sty(sty: sty, fldop: fn(t) -> t) -> sty {
       ty_rptr(r, tm) {
         ty_rptr(r, {ty: fldop(tm.ty), mutbl: tm.mutbl})
       }
-      ty_constr(subty, cs) {
-        ty_constr(fldop(subty), cs)
-      }
       ty_class(did, substs) {
         ty_class(did, fold_substs(substs, fldop))
       }
@@ -1589,7 +1559,6 @@ fn type_kind(cx: ctxt, ty: t) -> kind {
       ty_param(_, did) {
         param_bounds_to_kind(cx.ty_param_bounds.get(did.node))
       }
-      ty_constr(t, _) { type_kind(cx, t) }
       // FIXME (#2663): is self ever const?
       ty_self { kind_noncopyable() }
       ty_var(_) | ty_var_integral(_) {
@@ -1651,11 +1620,6 @@ fn is_instantiable(cx: ctxt, r_ty: t) -> bool {
           ty_unboxed_vec(_) {
             false
           }
-
-          ty_constr(t, _) {
-            type_requires(cx, seen, r_ty, t)
-          }
-
           ty_box(mt) |
           ty_uniq(mt) |
           ty_rptr(_, mt) {
@@ -1836,7 +1800,6 @@ fn type_is_pod(cx: ctxt, ty: t) -> bool {
       ty_evec(mt, vstore_fixed(_)) | ty_unboxed_vec(mt) {
         result = type_is_pod(cx, mt.ty);
       }
-      ty_constr(subt, _) { result = type_is_pod(cx, subt); }
       ty_param(_, _) { result = false; }
       ty_opaque_closure_ptr(_) { result = true; }
       ty_class(did, substs) {
@@ -1967,18 +1930,6 @@ fn hash_type_structure(st: sty) -> uint {
         for subtys.each |s| { h = (h << 2u) + type_id(s) }
         h
     }
-    fn hash_type_constr(id: uint, c: @type_constr) -> uint {
-        let mut h = id;
-        h = (h << 2u) + hash_def(h, c.node.id);
-        for c.node.args.each |a| {
-            alt a.node {
-              carg_base { h += h << 2u; }
-              carg_lit(_) { fail ~"lit args not implemented yet"; }
-              carg_ident(p) { h += h << 2u; }
-            }
-        }
-        h
-    }
     fn hash_region(r: region) -> uint {
         alt r { // no idea if this is any good
           re_bound(br) { (hash_bound_region(br)) << 2u | 0u }
@@ -2036,11 +1987,6 @@ fn hash_type_structure(st: sty) -> uint {
       ty_type { 32u }
       ty_bot { 34u }
       ty_ptr(mt) { hash_subty(35u, mt.ty) }
-      ty_constr(t, cs) {
-        let mut h = hash_subty(36u, t);
-        for cs.each |c| { h = (h << 2u) + hash_type_constr(h, c); }
-        h
-      }
       ty_uniq(mt) { hash_subty(37u, mt.ty) }
       ty_trait(did, substs) {
         let mut h = hash_def(40u, did);
@@ -2061,49 +2007,6 @@ fn hash_type_structure(st: sty) -> uint {
     }
 }
 
-fn arg_eq<T>(eq: fn(T, T) -> bool,
-             a: @sp_constr_arg<T>,
-             b: @sp_constr_arg<T>)
-   -> bool {
-    alt a.node {
-      ast::carg_base {
-        alt b.node { ast::carg_base { ret true; } _ { ret false; } }
-      }
-      ast::carg_ident(s) {
-        alt b.node { ast::carg_ident(t) { ret eq(s, t); } _ { ret false; } }
-      }
-      ast::carg_lit(l) {
-        alt b.node {
-          ast::carg_lit(m) { ret const_eval::lit_eq(l, m); } _ { ret false; }
-        }
-      }
-    }
-}
-
-fn args_eq<T>(eq: fn(T, T) -> bool,
-              a: ~[@sp_constr_arg<T>],
-              b: ~[@sp_constr_arg<T>]) -> bool {
-    let mut i: uint = 0u;
-    for a.each |arg| {
-        if !arg_eq(eq, arg, b[i]) { ret false; }
-        i += 1u;
-    }
-    ret true;
-}
-
-fn constr_eq(c: @constr, d: @constr) -> bool {
-    fn eq_int(&&x: uint, &&y: uint) -> bool { ret x == y; }
-    ret path_to_str(c.node.path) == path_to_str(d.node.path) &&
-            args_eq(eq_int, c.node.args, d.node.args);
-}
-
-fn constrs_eq(cs: ~[@constr], ds: ~[@constr]) -> bool {
-    if vec::len(cs) != vec::len(ds) { ret false; }
-    let mut i = 0u;
-    for cs.each |c| { if !constr_eq(c, ds[i]) { ret false; } i += 1u; }
-    ret true;
-}
-
 fn node_id_to_type(cx: ctxt, id: ast::node_id) -> t {
     alt smallintmap::find(*cx.node_types, id as uint) {
        some(t) { t }
@@ -2385,7 +2288,6 @@ fn ty_sort_str(cx: ctxt, t: t) -> ~str {
       ty_var_integral(_) { ~"integral variable" }
       ty_param(_, _) { ~"type parameter" }
       ty_self { ~"self" }
-      ty_constr(t, _) { ty_sort_str(cx, t) }
     }
 }
 
@@ -2443,16 +2345,6 @@ fn type_err_to_str(cx: ctxt, err: type_err) -> ~str {
         ret ~"expected argument mode " + mode_to_str(e_mode) +
             ~" but found " + mode_to_str(a_mode);
       }
-      terr_constr_len(e_len, a_len) {
-        ret ~"expected a type with " + uint::str(e_len) +
-            ~" constraints, but found one with " + uint::str(a_len) +
-            ~" constraints";
-      }
-      terr_constr_mismatch(e_constr, a_constr) {
-        ret ~"expected a type with constraint " + ty_constr_to_str(e_constr) +
-            ~" but found one with constraint " +
-            ty_constr_to_str(a_constr);
-      }
       terr_regions_differ(subregion, superregion) {
         ret #fmt("references with lifetime %s do not necessarily \
                   outlive references with lifetime %s",
@@ -2784,22 +2676,6 @@ pure fn is_public(f: field_ty) -> bool {
   }
 }
 
-// Look up the list of method names and IDs for a given class
-// Fails if the id is not bound to a class.
-fn lookup_class_method_ids(cx: ctxt, did: ast::def_id)
-    : is_local(did) -> ~[{name: ident, id: node_id, vis: visibility}] {
-    alt cx.items.find(did.node) {
-       some(ast_map::node_item(@{node: item_class(_,_,items,_,_), _}, _)) {
-         let (_,ms) = split_class_items(items);
-         vec::map(ms, |m| {name: m.ident, id: m.id,
-                            vis: m.vis})
-       }
-       _ {
-           cx.sess.bug(~"lookup_class_method_ids: id not bound to a class");
-       }
-    }
-}
-
 /* Given a class def_id and a method name, return the method's
  def_id. Needed so we can do static dispatch for methods
  Doesn't care about the method's privacy. (It's assumed that
@@ -2807,7 +2683,26 @@ fn lookup_class_method_ids(cx: ctxt, did: ast::def_id)
 */
 fn lookup_class_method_by_name(cx:ctxt, did: ast::def_id, name: ident,
                                sp: span) -> def_id {
-    if check is_local(did) {
+
+    // Look up the list of method names and IDs for a given class
+    // Fails if the id is not bound to a class.
+    fn lookup_class_method_ids(cx: ctxt, did: ast::def_id)
+        -> ~[{name: ident, id: node_id, vis: visibility}] {
+
+        assert is_local(did);
+        alt cx.items.find(did.node) {
+          some(ast_map::node_item(@{node: item_class(_,_,items,_,_), _}, _)) {
+            let (_,ms) = split_class_items(items);
+            vec::map(ms, |m| {name: m.ident, id: m.id,
+                              vis: m.vis})
+          }
+          _ {
+            cx.sess.bug(~"lookup_class_method_ids: id not bound to a class");
+          }
+        }
+    }
+
+    if is_local(did) {
        let ms = lookup_class_method_ids(cx, did);
         for ms.each |m| {
          if m.name == name {
@@ -2939,24 +2834,6 @@ fn is_binopable(_cx: ctxt, ty: t, op: ast::binop) -> bool {
     ret tbl[tycat(ty)][opcat(op)];
 }
 
-fn ast_constr_to_constr<T>(tcx: ctxt, c: @ast::constr_general<T>) ->
-   @constr_general<T> {
-    alt tcx.def_map.find(c.node.id) {
-      some(ast::def_fn(pred_id, ast::pure_fn)) {
-        ret @ast_util::respan(c.span,
-                              {path: c.node.path,
-                               args: c.node.args,
-                               id: pred_id});
-      }
-      _ {
-        tcx.sess.span_fatal(c.span,
-                            ~"predicate " + path_to_str(c.node.path) +
-                            ~" is unbound or bound to a non-function or an \
-            impure function");
-      }
-    }
-}
-
 fn ty_params_to_tys(tcx: ty::ctxt, tps: ~[ast::ty_param]) -> ~[t] {
     vec::from_fn(tps.len(), |i| {
                 ty::mk_param(tcx, i, ast_util::local_def(tps[i].id))
diff --git a/src/rustc/middle/typeck.rs b/src/rustc/middle/typeck.rs
index 1d86c47dddb..51f87c697a5 100644
--- a/src/rustc/middle/typeck.rs
+++ b/src/rustc/middle/typeck.rs
@@ -240,7 +240,7 @@ fn check_main_fn_ty(ccx: @crate_ctxt,
     let main_t = ty::node_id_to_type(tcx, main_id);
     alt ty::get(main_t).struct {
       ty::ty_fn({purity: ast::impure_fn, proto: ast::proto_bare,
-                 inputs, output, ret_style: ast::return_val, constraints}) {
+                 inputs, output, ret_style: ast::return_val}) {
         alt tcx.items.find(main_id) {
          some(ast_map::node_item(it,_)) {
              alt it.node {
@@ -254,8 +254,7 @@ fn check_main_fn_ty(ccx: @crate_ctxt,
          }
          _ {}
         }
-        let mut ok = vec::len(constraints) == 0u;
-        ok &= ty::type_is_nil(output);
+        let mut ok = ty::type_is_nil(output);
         let num_args = vec::len(inputs);
         ok &= num_args == 0u || num_args == 1u &&
               arg_is_argv_ty(tcx, inputs[0]);
diff --git a/src/rustc/middle/typeck/astconv.rs b/src/rustc/middle/typeck/astconv.rs
index b9325b3abee..1b1bf7732cb 100644
--- a/src/rustc/middle/typeck/astconv.rs
+++ b/src/rustc/middle/typeck/astconv.rs
@@ -332,13 +332,6 @@ fn ast_ty_to_ty<AC: ast_conv, RS: region_scope copy>(
             ast_ty.span,
             ~"implied fixed length for bound");
       }
-      ast::ty_constr(t, cs) {
-        let mut out_cs = ~[];
-        for cs.each |constr| {
-            vec::push(out_cs, ty::ast_constr_to_constr(tcx, constr));
-        }
-        ty::mk_constr(tcx, ast_ty_to_ty(self, rscope, t), out_cs)
-      }
       ast::ty_infer {
         // ty_infer should only appear as the type of arguments or return
         // values in a fn_expr, or as the type of local variables.  Both of
@@ -429,12 +422,8 @@ fn ty_of_fn_decl<AC: ast_conv, RS: region_scope copy>(
           _ {ast_ty_to_ty(self, rb, decl.output)}
         };
 
-        let out_constrs = vec::map(decl.constraints, |constr| {
-            ty::ast_constr_to_constr(self.tcx(), constr)
-        });
-
         {purity: decl.purity, proto: proto, inputs: input_tys,
-         output: output_ty, ret_style: decl.cf, constraints: out_constrs}
+         output: output_ty, ret_style: decl.cf}
     }
 }
 
diff --git a/src/rustc/middle/typeck/check.rs b/src/rustc/middle/typeck/check.rs
index c09616c264a..4f5ea3fe4f8 100644
--- a/src/rustc/middle/typeck/check.rs
+++ b/src/rustc/middle/typeck/check.rs
@@ -225,7 +225,6 @@ fn check_fn(ccx: @crate_ctxt,
     };
 
     gather_locals(fcx, decl, body, arg_tys);
-    check_constraints(fcx, decl.constraints, decl.inputs);
     check_block(fcx, body);
 
     // We unify the tail expr's type with the
@@ -1342,15 +1341,6 @@ fn check_expr_with_unifier(fcx: @fn_ctxt,
         check_expr(fcx, e, none);
         fcx.write_nil(id);
       }
-      ast::expr_check(_, e) {
-        bot = check_pred_expr(fcx, e);
-        fcx.write_nil(id);
-      }
-      ast::expr_if_check(cond, thn, elsopt) {
-        bot =
-            check_pred_expr(fcx, cond) |
-                check_then_else(fcx, thn, elsopt, id, expr.span);
-      }
       ast::expr_assert(e) {
         bot = check_expr_with(fcx, e, ty::mk_bool(tcx));
         fcx.write_nil(id);
@@ -1643,8 +1633,7 @@ fn check_expr_with_unifier(fcx: @fn_ctxt,
                                 proto: ast::proto_any,
                                 inputs: ~[{mode: m, ty: ty_nilp}],
                                 output: ty_nilp,
-                                ret_style: ast::return_val,
-                                constraints: ~[]})
+                                ret_style: ast::return_val})
             };
 
             demand::suptype(fcx, expr.span,
@@ -1893,119 +1882,6 @@ fn check_enum_variants(ccx: @crate_ctxt,
     check_instantiable(ccx.tcx, sp, id);
 }
 
-// A generic function for checking the pred in a check
-// or if-check
-fn check_pred_expr(fcx: @fn_ctxt, e: @ast::expr) -> bool {
-    let bot = check_expr_with(fcx, e, ty::mk_bool(fcx.ccx.tcx));
-
-    /* e must be a call expr where all arguments are either
-    literals or slots */
-    alt e.node {
-      ast::expr_call(operator, operands, _) {
-        if !ty::is_pred_ty(fcx.expr_ty(operator)) {
-            fcx.ccx.tcx.sess.span_err
-                (operator.span,
-                 ~"operator in constraint has non-boolean return type");
-        }
-
-        alt operator.node {
-          ast::expr_path(oper_name) {
-            alt fcx.ccx.tcx.def_map.find(operator.id) {
-              some(ast::def_fn(_, ast::pure_fn)) {
-                // do nothing
-              }
-              _ {
-                fcx.ccx.tcx.sess.span_err(operator.span,
-                                            ~"impure function as operator \
-                                             in constraint");
-              }
-            }
-            for operands.each |operand| {
-                if !ast_util::is_constraint_arg(operand) {
-                    let s =
-                        ~"constraint args must be slot variables or literals";
-                    fcx.ccx.tcx.sess.span_err(e.span, s);
-                }
-            }
-          }
-          _ {
-            let s = ~"in a constraint, expected the \
-                     constraint name to be an explicit name";
-            fcx.ccx.tcx.sess.span_err(e.span, s);
-          }
-        }
-      }
-      _ { fcx.ccx.tcx.sess.span_err(e.span, ~"check on non-predicate"); }
-    }
-    ret bot;
-}
-
-fn check_constraints(fcx: @fn_ctxt, cs: ~[@ast::constr],
-                     args: ~[ast::arg]) {
-    let num_args = vec::len(args);
-    for cs.each |c| {
-        let mut c_args = ~[];
-        for c.node.args.each |a| {
-            vec::push(c_args,
-                 // "base" should not occur in a fn type thing, as of
-                 // yet, b/c we don't allow constraints on the return type
-
-                 // Works b/c no higher-order polymorphism
-                 /*
-                 This is kludgy, and we probably shouldn't be assigning
-                 node IDs here, but we're creating exprs that are
-                 ephemeral, just for the purposes of typechecking. So
-                 that's my justification.
-                 */
-                 @alt a.node {
-                    ast::carg_base {
-                      fcx.ccx.tcx.sess.span_bug(a.span,
-                                                ~"check_constraints:\
-                    unexpected carg_base");
-                    }
-                    ast::carg_lit(l) {
-                      let tmp_node_id = fcx.ccx.tcx.sess.next_node_id();
-                      {id: tmp_node_id,
-                       callee_id: fcx.ccx.tcx.sess.next_node_id(),
-                       node: ast::expr_lit(l), span: a.span}
-                    }
-                    ast::carg_ident(i) {
-                      if i < num_args {
-                          let p = @{span: a.span, global: false,
-                                    idents: ~[args[i].ident],
-                                    rp: none, types: ~[]};
-                          let arg_occ_node_id =
-                              fcx.ccx.tcx.sess.next_node_id();
-                          fcx.ccx.tcx.def_map.insert
-                              (arg_occ_node_id,
-                               ast::def_arg(args[i].id, args[i].mode));
-                          {id: arg_occ_node_id,
-                           callee_id: fcx.ccx.tcx.sess.next_node_id(),
-                           node: ast::expr_path(p),
-                           span: a.span}
-                      } else {
-                          fcx.ccx.tcx.sess.span_bug(
-                              a.span, ~"check_constraints:\
-                                       carg_ident index out of bounds");
-                      }
-                    }
-                  });
-        }
-        let p_op: ast::expr_ = ast::expr_path(c.node.path);
-        let oper: @ast::expr = @{id: c.node.id,
-             callee_id: fcx.ccx.tcx.sess.next_node_id(),
-             node: p_op, span: c.span};
-        // Another ephemeral expr
-        let call_expr_id = fcx.ccx.tcx.sess.next_node_id();
-        let call_expr =
-            @{id: call_expr_id,
-              callee_id: fcx.ccx.tcx.sess.next_node_id(),
-              node: ast::expr_call(oper, c_args, false),
-              span: c.span};
-        check_pred_expr(fcx, call_expr);
-    }
-}
-
 // Determines whether the given node ID is a use of the def of
 // the self ID for the current method, if there is one
 // self IDs in an outer scope count. so that means that you can
@@ -2305,8 +2181,7 @@ fn check_intrinsic_type(ccx: @crate_ctxt, it: @ast::foreign_item) {
                     ty::mk_mach_uint(ccx.tcx, ast::ty_u8))
             }],
             output: ty::mk_nil(ccx.tcx),
-            ret_style: ast::return_val,
-            constraints: ~[]
+            ret_style: ast::return_val
         });
         (0u, ~[arg(ast::by_ref, fty)], ty::mk_nil(tcx))
       }
@@ -2319,8 +2194,7 @@ fn check_intrinsic_type(ccx: @crate_ctxt, it: @ast::foreign_item) {
     let fty = ty::mk_fn(tcx, {purity: ast::impure_fn,
                               proto: ast::proto_bare,
                               inputs: inputs, output: output,
-                              ret_style: ast::return_val,
-                              constraints: ~[]});
+                              ret_style: ast::return_val});
     let i_ty = ty::lookup_item_type(ccx.tcx, local_def(it.id));
     let i_n_tps = (*i_ty.bounds).len();
     if i_n_tps != n_tps {
diff --git a/src/rustc/middle/typeck/check/alt.rs b/src/rustc/middle/typeck/check/alt.rs
index 158d19bb6e2..2b32c8e3564 100644
--- a/src/rustc/middle/typeck/check/alt.rs
+++ b/src/rustc/middle/typeck/check/alt.rs
@@ -1,5 +1,6 @@
 import middle::typeck::infer::methods; // next_ty_var,
                                        // resolve_type_vars_if_possible
+import syntax::print::pprust;
 
 fn check_alt(fcx: @fn_ctxt,
              expr: @ast::expr,
@@ -124,6 +125,7 @@ fn check_pat_variant(pcx: pat_ctxt, pat: @ast::pat, path: @ast::path,
 fn check_pat(pcx: pat_ctxt, pat: @ast::pat, expected: ty::t) {
     let fcx = pcx.fcx;
     let tcx = pcx.fcx.ccx.tcx;
+
     alt pat.node {
       ast::pat_wild {
         fcx.write_ty(pat.id, expected);
diff --git a/src/rustc/middle/typeck/coherence.rs b/src/rustc/middle/typeck/coherence.rs
index ecc114cfc85..228bf408836 100644
--- a/src/rustc/middle/typeck/coherence.rs
+++ b/src/rustc/middle/typeck/coherence.rs
@@ -8,7 +8,7 @@ import middle::ty::{get, t, ty_box, ty_uniq, ty_ptr, ty_rptr, ty_enum};
 import middle::ty::{ty_class, ty_nil, ty_bot, ty_bool, ty_int, ty_uint};
 import middle::ty::{ty_float, ty_estr, ty_evec, ty_rec};
 import middle::ty::{ty_fn, ty_trait, ty_tup, ty_var, ty_var_integral};
-import middle::ty::{ty_param, ty_self, ty_constr, ty_type, ty_opaque_box};
+import middle::ty::{ty_param, ty_self, ty_type, ty_opaque_box};
 import middle::ty::{ty_opaque_closure_ptr, ty_unboxed_vec, new_ty_hash};
 import middle::ty::{subst};
 import middle::typeck::infer::{infer_ctxt, mk_subty, new_infer_ctxt};
@@ -173,7 +173,7 @@ class CoherenceChecker {
             ty_nil | ty_bot | ty_bool | ty_int(*) | ty_uint(*) | ty_float(*) |
             ty_estr(*) | ty_evec(*) | ty_rec(*) |
             ty_fn(*) | ty_tup(*) | ty_var(*) | ty_var_integral(*) |
-            ty_param(*) | ty_self | ty_constr(*) | ty_type | ty_opaque_box |
+            ty_param(*) | ty_self | ty_type | ty_opaque_box |
             ty_opaque_closure_ptr(*) | ty_unboxed_vec(*) {
                 none
             }
diff --git a/src/rustc/middle/typeck/collect.rs b/src/rustc/middle/typeck/collect.rs
index 64d477ae63f..68253a51ba6 100644
--- a/src/rustc/middle/typeck/collect.rs
+++ b/src/rustc/middle/typeck/collect.rs
@@ -126,8 +126,7 @@ fn get_enum_variant_types(ccx: @crate_ctxt,
                             proto: ast::proto_box,
                             inputs: args,
                             output: enum_ty,
-                            ret_style: ast::return_val,
-                            constraints: ~[]})
+                            ret_style: ast::return_val})
         };
         let tpt = {bounds: ty_param_bounds(ccx, ty_params),
                    rp: rp,
@@ -363,8 +362,7 @@ fn convert(ccx: @crate_ctxt, it: @ast::item) {
                   proto: ast::proto_any,
                   inputs: t_args,
                   output: t_res,
-                  ret_style: ast::return_val,
-                  constraints: ~[]}); // FIXME (#2813): allow ctors to have
+                  ret_style: ast::return_val});
         // constraints, or remove constraints from the language
         write_ty_to_tcx(tcx, ctor.node.id, t_ctor);
         tcx.tcache.insert(local_def(ctor.node.id),
@@ -618,8 +616,7 @@ fn ty_of_foreign_fn_decl(ccx: @crate_ctxt,
                                    proto: ast::proto_bare,
                                    inputs: input_tys,
                                    output: output_ty,
-                                   ret_style: ast::return_val,
-                                   constraints: ~[]});
+                                   ret_style: ast::return_val});
     let tpt = {bounds: bounds, rp: false, ty: t_fn};
     ccx.tcx.tcache.insert(def_id, tpt);
     ret tpt;
diff --git a/src/rustc/middle/typeck/infer.rs b/src/rustc/middle/typeck/infer.rs
index e88aecb6d5d..9b725072549 100644
--- a/src/rustc/middle/typeck/infer.rs
+++ b/src/rustc/middle/typeck/infer.rs
@@ -974,49 +974,6 @@ impl unify_methods for infer_ctxt {
         uok()
     }
 
-    fn constrs(
-        expected: @ty::type_constr,
-        actual_constr: @ty::type_constr) -> ures {
-
-        let err_res =
-            err(ty::terr_constr_mismatch(expected, actual_constr));
-
-        if expected.node.id != actual_constr.node.id { ret err_res; }
-        let expected_arg_len = vec::len(expected.node.args);
-        let actual_arg_len = vec::len(actual_constr.node.args);
-        if expected_arg_len != actual_arg_len { ret err_res; }
-        let mut i = 0u;
-        for expected.node.args.each |a| {
-            let actual = actual_constr.node.args[i];
-            alt a.node {
-              ast::carg_base {
-                alt actual.node {
-                  ast::carg_base { }
-                  _ { ret err_res; }
-                }
-              }
-              ast::carg_lit(l) {
-                alt actual.node {
-                  ast::carg_lit(m) {
-                    if l != m { ret err_res; }
-                  }
-                  _ { ret err_res; }
-                }
-              }
-              ast::carg_ident(p) {
-                alt actual.node {
-                  ast::carg_ident(q) {
-                    if p.idents != q.idents { ret err_res; }
-                  }
-                  _ { ret err_res; }
-                }
-              }
-            }
-            i += 1u;
-        }
-        ret uok();
-    }
-
     fn bnds<T:copy to_str st>(
         a: bound<T>, b: bound<T>) -> ures {
 
@@ -1035,18 +992,6 @@ impl unify_methods for infer_ctxt {
         }
     }
 
-    fn constrvecs(
-        as: ~[@ty::type_constr], bs: ~[@ty::type_constr]) -> ures {
-
-        if check vec::same_length(as, bs) {
-            do iter_vec2(as, bs) |a,b| {
-                self.constrs(a, b)
-            }
-        } else {
-            err(ty::terr_constr_len(bs.len(), as.len()))
-        }
-    }
-
     fn sub_tys(a: ty::t, b: ty::t) -> ures {
         sub(self).tys(a, b).chain(|_t| ok(()) )
     }
@@ -1584,7 +1529,7 @@ fn super_tps<C:combine>(
     // future we could allow type parameters to declare a
     // variance.
 
-    if check vec::same_length(as, bs) {
+    if vec::same_length(as, bs) {
         iter_vec2(as, bs, |a, b| {
             self.infcx().eq_tys(a, b)
         }).then(|| ok(as) )
@@ -1674,7 +1619,7 @@ fn super_fns<C:combine>(
     fn argvecs<C:combine>(self: C, a_args: ~[ty::arg],
                           b_args: ~[ty::arg]) -> cres<~[ty::arg]> {
 
-        if check vec::same_length(a_args, b_args) {
+        if vec::same_length(a_args, b_args) {
             map_vec2(a_args, b_args, |a, b| self.args(a, b) )
         } else {
             err(ty::terr_arg_count)
@@ -1693,8 +1638,7 @@ fn super_fns<C:combine>(
                             proto: p,
                             inputs: inputs,
                             output: output,
-                            ret_style: rs,
-                            constraints: a_f.constraints})
+                            ret_style: rs})
                     // }
                     }
                 }
@@ -1824,7 +1768,7 @@ fn super_tys<C:combine>(
       }
 
       (ty::ty_rec(as), ty::ty_rec(bs)) {
-        if check vec::same_length(as, bs) {
+        if vec::same_length(as, bs) {
             map_vec2(as, bs, |a,b| {
                 self.flds(a, b)
             }).chain(|flds| ok(ty::mk_rec(tcx, flds)) )
@@ -1834,7 +1778,7 @@ fn super_tys<C:combine>(
       }
 
       (ty::ty_tup(as), ty::ty_tup(bs)) {
-        if check vec::same_length(as, bs) {
+        if vec::same_length(as, bs) {
             map_vec2(as, bs, |a, b| self.tys(a, b) )
                 .chain(|ts| ok(ty::mk_tup(tcx, ts)) )
         } else {
@@ -1848,14 +1792,6 @@ fn super_tys<C:combine>(
         }
       }
 
-      (ty::ty_constr(a_t, a_constrs), ty::ty_constr(b_t, b_constrs)) {
-        do self.tys(a_t, b_t).chain |t| {
-            do self.infcx().constrvecs(a_constrs, b_constrs).then {
-                ok(ty::mk_constr(tcx, t, a_constrs))
-            }
-        }
-      }
-
       _ { err(ty::terr_sorts(b, a)) }
     }
 }
diff --git a/src/rustc/rustc.rc b/src/rustc/rustc.rc
index 4a3f017c83b..bf82cf59426 100644
--- a/src/rustc/rustc.rc
+++ b/src/rustc/rustc.rc
@@ -89,19 +89,6 @@ mod middle {
     mod region;
     mod const_eval;
     mod astencode;
-
-    mod tstate {
-        mod ck;
-        mod annotate;
-        #[path = "auxiliary.rs"]
-        mod aux;
-        mod bitvectors;
-        mod collect_locals;
-        mod pre_post_conditions;
-        mod states;
-        mod ann;
-        mod tritv;
-    }
 }
 
 mod front {
diff --git a/src/rustc/util/ppaux.rs b/src/rustc/util/ppaux.rs
index 3ed871dc701..04152eb69d3 100644
--- a/src/rustc/util/ppaux.rs
+++ b/src/rustc/util/ppaux.rs
@@ -1,9 +1,9 @@
 import std::map::hashmap;
 import middle::ty;
 import middle::ty::{arg, bound_region, br_anon, br_named, canon_mode};
-import middle::ty::{ck_block, ck_box, ck_uniq, constr, ctxt, field, method};
+import middle::ty::{ck_block, ck_box, ck_uniq, ctxt, field, method};
 import middle::ty::{mt, re_bound, re_free, re_scope, re_var, region, t};
-import middle::ty::{ty_bool, ty_bot, ty_box, ty_class, ty_constr, ty_enum};
+import middle::ty::{ty_bool, ty_bot, ty_box, ty_class, ty_enum};
 import middle::ty::{ty_estr, ty_evec, ty_float, ty_fn, ty_trait, ty_int};
 import middle::ty::{ty_nil, ty_opaque_box, ty_opaque_closure_ptr, ty_param};
 import middle::ty::{ty_ptr, ty_rec, ty_rptr, ty_self, ty_tup};
@@ -12,7 +12,7 @@ import middle::ty::{ty_unboxed_vec, vid};
 import metadata::encoder;
 import syntax::codemap;
 import syntax::print::pprust;
-import syntax::print::pprust::{path_to_str, constr_args_to_str, proto_to_str,
+import syntax::print::pprust::{path_to_str, proto_to_str,
                                mode_to_str, purity_to_str};
 import syntax::{ast, ast_util};
 import syntax::ast_map;
@@ -134,8 +134,7 @@ fn ty_to_str(cx: ctxt, typ: t) -> ~str {
     }
     fn fn_to_str(cx: ctxt, purity: ast::purity, proto: ast::proto,
                  ident: option<ast::ident>,
-                 inputs: ~[arg], output: t, cf: ast::ret_style,
-                 constrs: ~[@constr]) -> ~str {
+                 inputs: ~[arg], output: t, cf: ast::ret_style) -> ~str {
         let mut s;
 
         s = alt purity {
@@ -156,13 +155,12 @@ fn ty_to_str(cx: ctxt, typ: t) -> ~str {
               ast::return_val { s += ty_to_str(cx, output); }
             }
         }
-        s += constrs_str(constrs);
         ret s;
     }
     fn method_to_str(cx: ctxt, m: method) -> ~str {
         ret fn_to_str(
             cx, m.fty.purity, m.fty.proto, some(m.ident), m.fty.inputs,
-            m.fty.output, m.fty.ret_style, m.fty.constraints) + ~";";
+            m.fty.output, m.fty.ret_style) + ~";";
     }
     fn field_to_str(cx: ctxt, f: field) -> ~str {
         ret *f.ident + ~": " + mt_to_str(cx, f.mt);
@@ -211,7 +209,7 @@ fn ty_to_str(cx: ctxt, typ: t) -> ~str {
       }
       ty_fn(f) {
         fn_to_str(cx, f.purity, f.proto, none, f.inputs,
-                  f.output, f.ret_style, f.constraints)
+                  f.output, f.ret_style)
       }
       ty_var(v) { v.to_str() }
       ty_var_integral(v) { v.to_str() }
@@ -234,7 +232,6 @@ fn ty_to_str(cx: ctxt, typ: t) -> ~str {
       }
       ty_estr(vs) { vstore_ty_to_str(cx, ~"str", vs) }
       ty_opaque_box { ~"@?" }
-      ty_constr(t, _) { ~"@?" }
       ty_opaque_closure_ptr(ck_block) { ~"closure&" }
       ty_opaque_closure_ptr(ck_box) { ~"closure@" }
       ty_opaque_closure_ptr(ck_uniq) { ~"closure~" }
@@ -267,27 +264,6 @@ fn ty_to_short_str(cx: ctxt, typ: t) -> ~str {
     ret s;
 }
 
-fn constr_to_str(c: @constr) -> ~str {
-    ret path_to_str(c.node.path) +
-            pprust::constr_args_to_str(pprust::uint_to_str, c.node.args);
-}
-
-fn constrs_str(constrs: ~[@constr]) -> ~str {
-    let mut s = ~"";
-    let mut colon = true;
-    for constrs.each |c| {
-        if colon { s += ~" : "; colon = false; } else { s += ~", "; }
-        s += constr_to_str(c);
-    }
-    ret s;
-}
-
-fn ty_constr_to_str<Q>(c: @ast::spanned<ast::constr_general_<@ast::path, Q>>)
-   -> ~str {
-    ret path_to_str(c.node.path) +
-            constr_args_to_str::<@ast::path>(path_to_str, c.node.args);
-}
-
 // Local Variables:
 // mode: rust
 // fill-column: 78;
diff --git a/src/rustdoc/unindent_pass.rs b/src/rustdoc/unindent_pass.rs
index 52d91a7994f..26b785b6614 100644
--- a/src/rustdoc/unindent_pass.rs
+++ b/src/rustdoc/unindent_pass.rs
@@ -60,7 +60,7 @@ fn unindent(s: ~str) -> ~str {
         }
     };
 
-    if check vec::is_not_empty(lines) {
+    if vec::is_not_empty(lines) {
         let unindented = ~[str::trim(vec::head(lines))]
             + do par::anymap(vec::tail(lines)) |line| {
             if str::is_whitespace(line) {
diff --git a/src/test/compile-fail/fn-constraint.rs b/src/test/compile-fail/fn-constraint.rs
deleted file mode 100644
index 2843ef93ea6..00000000000
--- a/src/test/compile-fail/fn-constraint.rs
+++ /dev/null
@@ -1,10 +0,0 @@
-// error-pattern:precondition constraint (for example, uint::le(a, b)
-use std;
-import str::*;
-
-fn main() unsafe {
-    fn foo(_a: uint, _b: uint) : uint::le(_a, _b) {}
-    let a: uint = 4u;
-    let b: uint = 1u;
-    log(error, foo(a, b));
-}
diff --git a/src/test/compile-fail/if-check-precond-fail.rs b/src/test/compile-fail/if-check-precond-fail.rs
deleted file mode 100644
index 4545277e18d..00000000000
--- a/src/test/compile-fail/if-check-precond-fail.rs
+++ /dev/null
@@ -1,12 +0,0 @@
-// error-pattern:unsatisfied precondition constraint
-pure fn even(x: uint) -> bool {
-    if x < 2u {
-        ret false;
-    } else if x == 2u { ret true; } else { ret even(x - 2u); }
-}
-
-fn print_even(x: uint) : even(x) { log(debug, x); }
-
-fn foo(x: uint) { if check even(x) { fail; } else { print_even(x); } }
-
-fn main() { foo(3u); }
diff --git a/src/test/compile-fail/impure-pred.rs b/src/test/compile-fail/impure-pred.rs
deleted file mode 100644
index aef5080e3ae..00000000000
--- a/src/test/compile-fail/impure-pred.rs
+++ /dev/null
@@ -1,14 +0,0 @@
-// -*- rust -*-
-
-fn g() { }
-
-pure fn f(_q: int) -> bool {
-    g(); //~ ERROR access to impure function prohibited in pure context
-    ret true;
-}
-
-fn main() {
-    let x = 0;
-
-    check (f(x));
-}
diff --git a/src/test/compile-fail/liveness-unused.rs b/src/test/compile-fail/liveness-unused.rs
index 7db0a9fe171..28c531b3b81 100644
--- a/src/test/compile-fail/liveness-unused.rs
+++ b/src/test/compile-fail/liveness-unused.rs
@@ -35,10 +35,12 @@ fn f4() {
 }
 
 // leave this in here just to trigger compile-fail:
-pure fn is_even(i: int) -> bool { (i%2) == 0 }
-fn even(i: int) : is_even(i) -> int { i }
+class r {
+    let x: ();
+    new() { self.x = (); }
+    drop {}
+}
 fn main() {
-    let i: int = 4;
-    log(debug, false && { check is_even(i); true });
-    even(i); //~ ERROR unsatisfied precondition
+    let x = r();
+    fn@() { copy x; }; //~ ERROR copying a noncopyable value
 }
diff --git a/src/test/compile-fail/loop-pred-constraints.rs b/src/test/compile-fail/loop-pred-constraints.rs
deleted file mode 100644
index a55fe477ba7..00000000000
--- a/src/test/compile-fail/loop-pred-constraints.rs
+++ /dev/null
@@ -1,16 +0,0 @@
-// https://github.com/mozilla/rust/issues/2374
-// error-pattern:unsatisfied precondition constraint (for example, even(y
-
-
-fn print_even(y: int) : even(y) { log(debug, y); }
-
-pure fn even(y: int) -> bool { true }
-
-fn main() {
-    let mut y = 42;
-    check (even(y));
-    loop {
-        print_even(y);
-        loop { y += 1; break; }
-    }
-}
diff --git a/src/test/compile-fail/no-constraint-prop.rs b/src/test/compile-fail/no-constraint-prop.rs
deleted file mode 100644
index f1c02bd406f..00000000000
--- a/src/test/compile-fail/no-constraint-prop.rs
+++ /dev/null
@@ -1,18 +0,0 @@
-// error-pattern:unsatisfied precondition constraint (for example, uint::le
-
-fn main() unsafe {
-    fn foo(_a: uint, _b: uint) : uint::le(_a, _b) {}
-    let mut a: uint = 1u;
-    let mut b: uint = 4u;
-    let mut c: uint = 5u;
-    // make sure that the constraint le(b, a) exists...
-    check (uint::le(b, a));
-    // ...invalidate it...
-    b += 1u;
-    check (uint::le(c, a));
-    // ...and check that it doesn't get set in the poststate of
-    // the next statement, since it's not true in the
-    // prestate.
-    let d <- a;
-    log(debug, foo(b, d));
-}
diff --git a/src/test/compile-fail/nonsense-constraints.rs b/src/test/compile-fail/nonsense-constraints.rs
deleted file mode 100644
index 2ac5ac128fc..00000000000
--- a/src/test/compile-fail/nonsense-constraints.rs
+++ /dev/null
@@ -1,13 +0,0 @@
-// Tests that the typechecker checks constraints
-// error-pattern:mismatched types: expected `uint` but found `u8`
-use std;
-import uint;
-
-fn enum_chars(start: u8, end: u8) : uint::le(start, end) -> ~[char] {
-    let i = start;
-    let r = ~[];
-    while i <= end { r += ~[i as char]; i += 1u as u8; }
-    ret r;
-}
-
-fn main() { log(debug, enum_chars('a' as u8, 'z' as u8)); }
diff --git a/src/test/compile-fail/not-a-pred-2.rs b/src/test/compile-fail/not-a-pred-2.rs
deleted file mode 100644
index 3bac354fb24..00000000000
--- a/src/test/compile-fail/not-a-pred-2.rs
+++ /dev/null
@@ -1,14 +0,0 @@
-// -*- rust -*-
-
-// error-pattern: non-predicate
-
-fn main() {
-    check (1 ==
-               2); // should fail to typecheck, as (a == b)
-                   // is not a manifest call
-
-
-
-
-
-}
diff --git a/src/test/compile-fail/not-a-pred-check.rs b/src/test/compile-fail/not-a-pred-check.rs
deleted file mode 100644
index 24016a70b2d..00000000000
--- a/src/test/compile-fail/not-a-pred-check.rs
+++ /dev/null
@@ -1,10 +0,0 @@
-// -*- rust -*-
-// error-pattern:impure function as operator
-
-fn f(q: int) -> bool { ret true; }
-
-fn main() {
-    let x = 0;
-
-    check (f(x));
-}
diff --git a/src/test/compile-fail/not-pred-args.rs b/src/test/compile-fail/not-pred-args.rs
deleted file mode 100644
index 6fb5273e1e7..00000000000
--- a/src/test/compile-fail/not-pred-args.rs
+++ /dev/null
@@ -1,11 +0,0 @@
-// -*- rust -*-
-
-// error-pattern:constraint args must be
-
-pure fn f(q: int) -> bool { ret true; }
-
-fn main() {
-    // should fail to typecheck, as pred args must be slot variables
-    // or literals
-    check (f(42 * 17));
-}
diff --git a/src/test/compile-fail/pred-assign.rs b/src/test/compile-fail/pred-assign.rs
deleted file mode 100644
index 19a71050986..00000000000
--- a/src/test/compile-fail/pred-assign.rs
+++ /dev/null
@@ -1,16 +0,0 @@
-// -*- rust -*-
-
-// error-pattern:unsatisfied precondition constraint (for example, lt(a, b)
-
-fn f(a: int, b: int) : lt(a, b) { }
-
-pure fn lt(a: int, b: int) -> bool { ret a < b; }
-
-fn main() {
-    let mut a: int = 10;
-    let mut b: int = 23;
-    let mut c: int = 77;
-    check (lt(a, b));
-    a = 24;
-    f(a, b);
-}
diff --git a/src/test/compile-fail/pred-on-wrong-slots.rs b/src/test/compile-fail/pred-on-wrong-slots.rs
deleted file mode 100644
index 3d887e8d6ef..00000000000
--- a/src/test/compile-fail/pred-on-wrong-slots.rs
+++ /dev/null
@@ -1,17 +0,0 @@
-// -*- rust -*-
-
-// error-pattern: lt(a, c)
-
-fn f(a: int, b: int) : lt(a, b) { }
-
-pure fn lt(a: int, b: int) -> bool { ret a < b; }
-
-fn main() {
-    let a: int = 10;
-    let b: int = 23;
-    let c: int = 77;
-    check (lt(a, b));
-    check (lt(b, c));
-    f(a, b);
-    f(a, c);
-}
diff --git a/src/test/compile-fail/pred-swap.rs b/src/test/compile-fail/pred-swap.rs
deleted file mode 100644
index b62f5a942f7..00000000000
--- a/src/test/compile-fail/pred-swap.rs
+++ /dev/null
@@ -1,16 +0,0 @@
-// -*- rust -*-
-
-// error-pattern:unsatisfied precondition constraint (for example, lt(a, b)
-
-fn f(a: int, b: int) : lt(a, b) { }
-
-pure fn lt(a: int, b: int) -> bool { ret a < b; }
-
-fn main() {
-    let mut a: int = 10;
-    let mut b: int = 23;
-    let mut c: int = 77;
-    check (lt(a, b));
-    b <-> a;
-    f(a, b);
-}
diff --git a/src/test/compile-fail/slot-as-pred.rs b/src/test/compile-fail/slot-as-pred.rs
deleted file mode 100644
index 820ebd655f5..00000000000
--- a/src/test/compile-fail/slot-as-pred.rs
+++ /dev/null
@@ -1,12 +0,0 @@
-// -*- rust -*-
-// error-pattern: unresolved name: lt
-
-fn f(a: int, b: int) : lt(a, b) { }
-
-fn main() {
-    let lt: int;
-    let a: int = 10;
-    let b: int = 23;
-    check (lt(a, b));
-    f(a, b);
-}
diff --git a/src/test/compile-fail/tstate-and-init.rs b/src/test/compile-fail/tstate-and-init.rs
deleted file mode 100644
index d6e01f20ff4..00000000000
--- a/src/test/compile-fail/tstate-and-init.rs
+++ /dev/null
@@ -1,7 +0,0 @@
-pure fn is_even(i: int) -> bool { (i%2) == 0 }
-fn even(i: int) : is_even(i) -> int { i }
-fn main() {
-    let i: int = 4;
-    log(debug, false && { check is_even(i); true });
-    even(i); //~ ERROR unsatisfied precondition
-}
diff --git a/src/test/compile-fail/tstate-block-uninit.rs b/src/test/compile-fail/tstate-block-uninit.rs
deleted file mode 100644
index 91a31fed6cf..00000000000
--- a/src/test/compile-fail/tstate-block-uninit.rs
+++ /dev/null
@@ -1,11 +0,0 @@
-pure fn is_even(i: int) -> bool { (i%2) == 0 }
-fn even(i: int) : is_even(i) -> int { i }
-
-fn force(f: fn()) { f(); }
-
-fn main() {
-    let x: int = 4;
-    force(fn&() {
-        even(x); //~ ERROR unsatisfied precondition
-    });
-}
diff --git a/src/test/compile-fail/tstate-break-uninit-2.rs b/src/test/compile-fail/tstate-break-uninit-2.rs
deleted file mode 100644
index 7d75009098f..00000000000
--- a/src/test/compile-fail/tstate-break-uninit-2.rs
+++ /dev/null
@@ -1,16 +0,0 @@
-pure fn is_even(i: int) -> bool { (i%2) == 0 }
-fn even(i: int) : is_even(i) -> int { i }
-
-fn foo() -> int {
-    let x: int = 4;
-
-    while 1 != 2 {
-        break;
-        check is_even(x); //~ WARNING unreachable statement
-    }
-
-    even(x); //~ ERROR unsatisfied precondition
-    ret 17;
-}
-
-fn main() { log(debug, foo()); }
diff --git a/src/test/compile-fail/tstate-break-uninit.rs b/src/test/compile-fail/tstate-break-uninit.rs
deleted file mode 100644
index b0d51deb5df..00000000000
--- a/src/test/compile-fail/tstate-break-uninit.rs
+++ /dev/null
@@ -1,16 +0,0 @@
-pure fn is_even(i: int) -> bool { (i%2) == 0 }
-fn even(i: int) : is_even(i) -> int { i }
-
-fn foo() -> int {
-    let x: int = 4;
-
-    loop {
-        break;
-        check is_even(x); //~ WARNING unreachable statement
-    }
-
-    even(x); //~ ERROR unsatisfied precondition
-    ret 17;
-}
-
-fn main() { log(debug, foo()); }
diff --git a/src/test/compile-fail/tstate-ctor-unsat.rs b/src/test/compile-fail/tstate-ctor-unsat.rs
deleted file mode 100644
index e72e57f901b..00000000000
--- a/src/test/compile-fail/tstate-ctor-unsat.rs
+++ /dev/null
@@ -1,25 +0,0 @@
-pure fn is_even(i: int) -> bool { (i%2) == 0 }
-fn even(i: int) : is_even(i) -> int { i }
-
-class cat {
-  priv {
-    let mut meows : uint;
-  }
-
-  let how_hungry : int;
-
-  fn eat() {
-    self.how_hungry -= 5;
-  }
-
-  new(in_x : uint, in_y : int) {
-    let foo = 3;
-    self.meows = in_x + (in_y as uint);
-    self.how_hungry = even(foo); //~ ERROR unsatisfied precondition
-  }
-}
-
-fn main() {
-  let nyan : cat = cat(52u, 99);
-  nyan.eat();
-}
diff --git a/src/test/compile-fail/tstate-fru.rs b/src/test/compile-fail/tstate-fru.rs
deleted file mode 100644
index c5335ce1f85..00000000000
--- a/src/test/compile-fail/tstate-fru.rs
+++ /dev/null
@@ -1,14 +0,0 @@
-// -*- rust -*-
-
-type point = {x: int, y: int};
-
-pure fn test(_p: point) -> bool { true }
-fn tested(p: point) : test(p) -> point { p }
-
-fn main() {
-    let origin: point;
-    origin = {x: 0, y: 0};
-    let right: point = {x: 10 with tested(origin)};
-        //~^ ERROR precondition
-    copy right;
-}
diff --git a/src/test/compile-fail/tstate-if-no-else.rs b/src/test/compile-fail/tstate-if-no-else.rs
deleted file mode 100644
index e9873110a44..00000000000
--- a/src/test/compile-fail/tstate-if-no-else.rs
+++ /dev/null
@@ -1,10 +0,0 @@
-pure fn is_even(i: int) -> bool { (i%2) == 0 }
-fn even(i: int) : is_even(i) -> int { i }
-
-fn foo(x: int) { log(debug, x); }
-
-fn main() {
-	let x: int = 10;
-        if 1 > 2 { check is_even(x); }
-        even(x); //~ ERROR unsatisfied precondition
-}
diff --git a/src/test/compile-fail/tstate-if-with-else.rs b/src/test/compile-fail/tstate-if-with-else.rs
deleted file mode 100644
index c813d84d465..00000000000
--- a/src/test/compile-fail/tstate-if-with-else.rs
+++ /dev/null
@@ -1,14 +0,0 @@
-pure fn is_even(i: int) -> bool { (i%2) == 0 }
-fn even(i: int) : is_even(i) -> int { i }
-
-fn foo(x: int) { log(debug, x); }
-
-fn main() {
-    let x: int = 10;
-    if 1 > 2 {
-        #debug("whoops");
-    } else {
-        check is_even(x);
-    }
-    even(x); //~ ERROR unsatisfied precondition
-}
diff --git a/src/test/compile-fail/tstate-loop-constraints.rs b/src/test/compile-fail/tstate-loop-constraints.rs
deleted file mode 100644
index 731a7d0b6d8..00000000000
--- a/src/test/compile-fail/tstate-loop-constraints.rs
+++ /dev/null
@@ -1,19 +0,0 @@
-pure fn is_even(i: int) -> bool { (i%2) == 0 }
-fn even(i: int) : is_even(i) -> int { i }
-
-fn main() {
-
-    let mut x: int = 42;
-    loop {
-        loop {
-            loop {
-                check is_even(x);
-                even(x); // OK
-                loop {
-                    even(x); //~ ERROR unsatisfied precondition
-                    x = 11; 
-                }
-            }
-        }
-    }
-}
diff --git a/src/test/compile-fail/tstate-or-init.rs b/src/test/compile-fail/tstate-or-init.rs
deleted file mode 100644
index f24dd9d888e..00000000000
--- a/src/test/compile-fail/tstate-or-init.rs
+++ /dev/null
@@ -1,7 +0,0 @@
-pure fn is_even(i: int) -> bool { (i%2) == 0 }
-fn even(i: int) : is_even(i) -> int { i }
-fn main() {
-    let i: int = 4;
-    log(debug, false || { check is_even(i); true });
-    even(i); //~ ERROR unsatisfied precondition
-}
diff --git a/src/test/compile-fail/tstate-return.rs b/src/test/compile-fail/tstate-return.rs
deleted file mode 100644
index 0ac68559f8b..00000000000
--- a/src/test/compile-fail/tstate-return.rs
+++ /dev/null
@@ -1,9 +0,0 @@
-pure fn is_even(i: int) -> bool { (i%2) == 0 }
-fn even(i: int) : is_even(i) -> int { i }
-
-fn f() -> int {
-	let x: int = 4;
-	ret even(x); //~ ERROR unsatisfied precondition
-}
-
-fn main() { f(); }
diff --git a/src/test/compile-fail/tstate-unsat-after-item.rs b/src/test/compile-fail/tstate-unsat-after-item.rs
deleted file mode 100644
index 6722736dea0..00000000000
--- a/src/test/compile-fail/tstate-unsat-after-item.rs
+++ /dev/null
@@ -1,9 +0,0 @@
-pure fn is_even(i: int) -> bool { (i%2) == 0 }
-fn even(i: int) : is_even(i) -> int { i }
-
-fn main() {
-    let x = 4;
-    fn baz(_x: int) { }
-    baz(even(x)); //~ ERROR unsatisfied precondition
-}
-
diff --git a/src/test/compile-fail/tstate-unsat-in-called-fn-expr.rs b/src/test/compile-fail/tstate-unsat-in-called-fn-expr.rs
deleted file mode 100644
index 3caee2475a8..00000000000
--- a/src/test/compile-fail/tstate-unsat-in-called-fn-expr.rs
+++ /dev/null
@@ -1,9 +0,0 @@
-fn foo(v: ~[int]) : vec::is_empty(v) { #debug("%d", v[0]); }
-
-fn main() {
-    let f = fn@() {
-        let v = ~[1];
-        foo(v); //~ ERROR unsatisfied precondition constraint
-    }();
-    log(error, f);
-}
diff --git a/src/test/compile-fail/tstate-unsat-in-fn-expr.rs b/src/test/compile-fail/tstate-unsat-in-fn-expr.rs
deleted file mode 100644
index ffc1e87bcc5..00000000000
--- a/src/test/compile-fail/tstate-unsat-in-fn-expr.rs
+++ /dev/null
@@ -1,9 +0,0 @@
-fn foo(v: ~[int]) : vec::is_empty(v) { #debug("%d", v[0]); }
-
-fn main() {
-    let f = fn@() {
-        let v = ~[1];
-        foo(v); //~ ERROR unsatisfied precondition constraint
-    };
-    log(error, f());
-}
diff --git a/src/test/compile-fail/tstate-unsat.rs b/src/test/compile-fail/tstate-unsat.rs
deleted file mode 100644
index 210feb28b92..00000000000
--- a/src/test/compile-fail/tstate-unsat.rs
+++ /dev/null
@@ -1,7 +0,0 @@
-pure fn is_even(i: int) -> bool { (i%2) == 0 }
-fn even(i: int) : is_even(i) -> int { i }
-
-fn main() {
-    let x: int = 4;
-    even(x); //~ ERROR unsatisfied precondition
-}
diff --git a/src/test/compile-fail/tstate-while-break.rs b/src/test/compile-fail/tstate-while-break.rs
deleted file mode 100644
index 49905d50348..00000000000
--- a/src/test/compile-fail/tstate-while-break.rs
+++ /dev/null
@@ -1,15 +0,0 @@
-pure fn is_even(i: int) -> bool { (i%2) == 0 }
-fn even(i: int) : is_even(i) -> int { i }
-
-fn test(cond: bool) {
-    let v = 4;
-    while cond {
-        check is_even(v);
-        break;
-    }
-    even(v); //~ ERROR unsatisfied precondition
-}
-
-fn main() {
-    test(true);
-}
diff --git a/src/test/compile-fail/tstate-while-cond.rs b/src/test/compile-fail/tstate-while-cond.rs
deleted file mode 100644
index afc77fa42c6..00000000000
--- a/src/test/compile-fail/tstate-while-cond.rs
+++ /dev/null
@@ -1,7 +0,0 @@
-pure fn is_even(i: int) -> bool { (i%2) == 0 }
-fn even(i: int) : is_even(i) -> int { i }
-
-fn main() {
-    let x: int = 4;
-    while even(x) != 0 { } //~ ERROR unsatisfied precondition
-}
diff --git a/src/test/compile-fail/tstate-while-loop-unsat-constriants.rs b/src/test/compile-fail/tstate-while-loop-unsat-constriants.rs
deleted file mode 100644
index 5fff9aa9cb5..00000000000
--- a/src/test/compile-fail/tstate-while-loop-unsat-constriants.rs
+++ /dev/null
@@ -1,16 +0,0 @@
-// error-pattern:unsatisfied precondition constraint (for example, even(y
-
-fn print_even(y: int) : even(y) { log(debug, y); }
-
-pure fn even(y: int) -> bool { true }
-
-fn main() {
-
-    let mut y: int = 42;
-    let mut x: int = 1;
-    check (even(y));
-    loop {
-        print_even(y);
-        while true { while true { while true { y += x; } } }
-    }
-}
diff --git a/src/test/compile-fail/tstate-while.rs b/src/test/compile-fail/tstate-while.rs
deleted file mode 100644
index f99c966aaf4..00000000000
--- a/src/test/compile-fail/tstate-while.rs
+++ /dev/null
@@ -1,10 +0,0 @@
-pure fn is_even(i: int) -> bool { (i%2) == 0 }
-fn even(i: int) : is_even(i) -> int { i }
-
-fn f() {
-    let mut x: int = 10;
-    while 1 == 1 { x = 10; }
-    even(x); //~ ERROR unsatisfied precondition
-}
-
-fn main() { f(); }
diff --git a/src/test/run-fail/fn-constraint-claim.rs b/src/test/run-fail/fn-constraint-claim.rs
deleted file mode 100644
index e209a3de489..00000000000
--- a/src/test/run-fail/fn-constraint-claim.rs
+++ /dev/null
@@ -1,7 +0,0 @@
-// error-pattern:quux
-use std;
-import uint::*;
-
-fn nop(a: uint, b: uint) : le(a, b) { fail ~"quux"; }
-
-fn main() { let a: uint = 5u; let b: uint = 4u; claim (le(a, b)); nop(a, b); }
diff --git a/src/test/run-fail/fn-constraint.rs b/src/test/run-fail/fn-constraint.rs
deleted file mode 100644
index f24d96e13cc..00000000000
--- a/src/test/run-fail/fn-constraint.rs
+++ /dev/null
@@ -1,9 +0,0 @@
-// error-pattern:Predicate uint::le(a, b) failed
-
-fn main() unsafe {
-    fn foo(_a: uint, _b: uint) : uint::le(_a, _b) {}
-    let a: uint = 4u;
-    let b: uint = 1u;
-    check (uint::le(a, b));
-    log(error, foo(a, b));
-}
diff --git a/src/test/run-fail/if-check-fail.rs b/src/test/run-fail/if-check-fail.rs
index 3aa87f04e2d..0ca92ab18c4 100644
--- a/src/test/run-fail/if-check-fail.rs
+++ b/src/test/run-fail/if-check-fail.rs
@@ -6,7 +6,7 @@ pure fn even(x: uint) -> bool {
 }
 
 fn foo(x: uint) {
-    if check even(x) {
+    if even(x) {
         log(debug, x);
     } else {
         fail ~"Number is odd";
diff --git a/src/test/run-fail/pred.rs b/src/test/run-fail/pred.rs
deleted file mode 100644
index 494bee968f1..00000000000
--- a/src/test/run-fail/pred.rs
+++ /dev/null
@@ -1,7 +0,0 @@
-// -*- rust -*-
-// error-pattern:Predicate lt(b, a) failed
-fn f(a: int, b: int) { }
-
-pure fn lt(a: int, b: int) -> bool { ret a < b; }
-
-fn main() { let a: int = 10; let b: int = 23; check (lt(b, a)); f(b, a); }
diff --git a/src/test/run-fail/unwind-check.rs b/src/test/run-fail/unwind-check.rs
deleted file mode 100644
index e01cc969cea..00000000000
--- a/src/test/run-fail/unwind-check.rs
+++ /dev/null
@@ -1,8 +0,0 @@
-// error-pattern:fail
-
-pure fn p(a: @int) -> bool { false }
-
-fn main() {
-    let a = @0;
-    check p(a);
-}
\ No newline at end of file
diff --git a/src/test/run-fail/zip-different-lengths.rs b/src/test/run-fail/zip-different-lengths.rs
index ae98291777a..5f29e83f8f8 100644
--- a/src/test/run-fail/zip-different-lengths.rs
+++ b/src/test/run-fail/zip-different-lengths.rs
@@ -1,6 +1,6 @@
 // In this case, the code should compile but
-// the check should fail at runtime
-// error-pattern:Predicate same_length
+// the assert should fail at runtime
+// error-pattern:Assertion same_length(chars, ints) failed
 use std;
 import uint;
 import u8;
@@ -25,12 +25,12 @@ fn enum_uints(start: uint, end: uint) -> ~[uint] {
 fn main() {
     let a = 'a' as u8, j = 'j' as u8, k = 1u, l = 9u;
     // Silly, but necessary
-    check (u8::le(a, j));
-    check (uint::le(k, l));
+    assert (u8::le(a, j));
+    assert (uint::le(k, l));
     let chars = enum_chars(a, j);
     let ints = enum_uints(k, l);
 
-    check (same_length(chars, ints));
+    assert (same_length(chars, ints));
     let ps = zip(chars, ints);
     fail ~"the impossible happened";
 }
diff --git a/src/test/run-pass/bug-862.rs b/src/test/run-pass/bug-862.rs
deleted file mode 100644
index 8172cae6b47..00000000000
--- a/src/test/run-pass/bug-862.rs
+++ /dev/null
@@ -1,7 +0,0 @@
-pure fn p(j: int) -> bool { true }
-
-fn f(i: int, j: int) : p(j) -> int { j }
-
-fn g(i: int, j: int) : p(j) -> int { f(i, j) }
-
-fn main() { let x = 1; check (p(x)); log(debug, g(x, x)); }
diff --git a/src/test/run-pass/check-pattern-bound.rs b/src/test/run-pass/check-pattern-bound.rs
deleted file mode 100644
index 936947701ad..00000000000
--- a/src/test/run-pass/check-pattern-bound.rs
+++ /dev/null
@@ -1,9 +0,0 @@
-use std;
-
-pure fn p(x: int) -> bool { true }
-
-fn f(x: int) : p(x) { }
-
-fn main() {
-    alt some(5) { some(y) { check (p(y)); f(y); } _ { fail ~"yuck"; } }
-}
diff --git a/src/test/run-pass/claim-nonterm.rs b/src/test/run-pass/claim-nonterm.rs
deleted file mode 100644
index 5f427d185eb..00000000000
--- a/src/test/run-pass/claim-nonterm.rs
+++ /dev/null
@@ -1,7 +0,0 @@
-// tests that the pred in a claim isn't actually eval'd
-use std;
-import uint::*;
-
-pure fn fails(a: uint) -> bool { fail; }
-
-fn main() { let b: uint = 4u; claim (fails(b)); }
diff --git a/src/test/run-pass/constrained-type.rs b/src/test/run-pass/constrained-type.rs
deleted file mode 100644
index c29bcbdfee2..00000000000
--- a/src/test/run-pass/constrained-type.rs
+++ /dev/null
@@ -1,11 +0,0 @@
-// -*- rust -*-
-
-enum list { cons(int, @list), nil, }
-
-type bubu = {x: int, y: int};
-
-pure fn less_than(x: int, y: int) -> bool { ret x < y; }
-
-type ordered_range = {low: int, high: int}  : less_than(*.low, *.high);
-
-fn main() { }
diff --git a/src/test/run-pass/constraint-prop-expr-move.rs b/src/test/run-pass/constraint-prop-expr-move.rs
deleted file mode 100644
index a2550197d0e..00000000000
--- a/src/test/run-pass/constraint-prop-expr-move.rs
+++ /dev/null
@@ -1,10 +0,0 @@
-
-fn main() unsafe {
-    fn foo(_a: uint, _b: uint) : uint::le(_a, _b) {}
-    let a: uint = 1u;
-    let b: uint = 4u;
-    let mut c: uint = 17u;
-    check (uint::le(a, b));
-    c <- a;
-    log(debug, foo(c, b));
-}
diff --git a/src/test/run-pass/constraint-prop-move.rs b/src/test/run-pass/constraint-prop-move.rs
deleted file mode 100644
index a07b60799e8..00000000000
--- a/src/test/run-pass/constraint-prop-move.rs
+++ /dev/null
@@ -1,8 +0,0 @@
-fn main() unsafe {
-    fn foo(_a: uint, _b: uint) : uint::le(_a, _b) {}
-    let a: uint = 1u;
-    let b: uint = 4u;
-    check (uint::le(a, b));
-    let c <- a;
-    log(debug, foo(c, b));
-}
diff --git a/src/test/run-pass/constraint-prop-swap.rs b/src/test/run-pass/constraint-prop-swap.rs
deleted file mode 100644
index 76d6a733e98..00000000000
--- a/src/test/run-pass/constraint-prop-swap.rs
+++ /dev/null
@@ -1,8 +0,0 @@
-fn main() unsafe {
-    fn foo(_a: uint, _b: uint) : uint::le(_a, _b) {}
-    let mut a: uint = 4u;
-    let mut b: uint = 1u;
-    check (uint::le(b, a));
-    b <-> a;
-    log(debug, foo(a, b));
-}
diff --git a/src/test/run-pass/constraint-prop.rs b/src/test/run-pass/constraint-prop.rs
deleted file mode 100644
index 6d5808be3d1..00000000000
--- a/src/test/run-pass/constraint-prop.rs
+++ /dev/null
@@ -1,8 +0,0 @@
-fn main() unsafe {
-    fn foo(_a: uint, _b: uint) : uint::le(_a, _b) {}
-    let a: uint = 1u;
-    let b: uint = 4u;
-    check uint::le(a, b);
-    let c = b;
-    log(debug, foo(a, c));
-}
diff --git a/src/test/run-pass/fn-constraint.rs b/src/test/run-pass/fn-constraint.rs
deleted file mode 100644
index 476a6b74a3d..00000000000
--- a/src/test/run-pass/fn-constraint.rs
+++ /dev/null
@@ -1,7 +0,0 @@
-fn main() unsafe {
-    fn foo(_a: uint, _b: uint) : uint::le(_a, _b) {}
-    let a: uint = 1u;
-    let b: uint = 4u;
-    check (uint::le(a, b));
-    log(debug, foo(a, b));
-}
diff --git a/src/test/run-pass/if-check-precond.rs b/src/test/run-pass/if-check-precond.rs
deleted file mode 100644
index f3d35f52a3a..00000000000
--- a/src/test/run-pass/if-check-precond.rs
+++ /dev/null
@@ -1,11 +0,0 @@
-pure fn even(x: uint) -> bool {
-    if x < 2u {
-        ret false;
-    } else if x == 2u { ret true; } else { ret even(x - 2u); }
-}
-
-fn print_even(x: uint) : even(x) { log(debug, x); }
-
-fn foo(x: uint) { if check even(x) { print_even(x); } else { fail; } }
-
-fn main() { foo(2u); }
diff --git a/src/test/run-pass/if-check.rs b/src/test/run-pass/if-check.rs
index 59766164018..78208ec6149 100644
--- a/src/test/run-pass/if-check.rs
+++ b/src/test/run-pass/if-check.rs
@@ -5,7 +5,7 @@ pure fn even(x: uint) -> bool {
 }
 
 fn foo(x: uint) {
-    if check even(x) {
+    if even(x) {
         log(debug, x);
     } else {
         fail;
diff --git a/src/test/run-pass/issue-933.rs b/src/test/run-pass/issue-933.rs
deleted file mode 100644
index 53d94d31506..00000000000
--- a/src/test/run-pass/issue-933.rs
+++ /dev/null
@@ -1,2 +0,0 @@
-pure fn c() -> bool { check c(); true }
-fn main() {}
diff --git a/src/test/run-pass/issue-970.rs b/src/test/run-pass/issue-970.rs
deleted file mode 100644
index 17fa82980a9..00000000000
--- a/src/test/run-pass/issue-970.rs
+++ /dev/null
@@ -1,6 +0,0 @@
-enum maybe_ordered_pair {
-    yes({low: int, high: int} : less_than(*.low, *.high)),
-    no
-}
-pure fn less_than(x: int, y: int) -> bool { ret x < y; }
-fn main() { }
diff --git a/src/test/run-pass/non-boolean-pure-fns.rs b/src/test/run-pass/non-boolean-pure-fns.rs
index 86a06ab5aa5..da3f19062dd 100644
--- a/src/test/run-pass/non-boolean-pure-fns.rs
+++ b/src/test/run-pass/non-boolean-pure-fns.rs
@@ -10,19 +10,13 @@ pure fn pure_length<T: copy>(ls: @list<T>) -> uint { pure_length_go(ls, 0u) }
 
 pure fn nonempty_list<T: copy>(ls: @list<T>) -> bool { pure_length(ls) > 0u }
 
-// Of course, the compiler can't take advantage of the
-// knowledge that ls is a cons node. Future work.
-// Also, this is pretty contrived since nonempty_list
-// could be a "enum refinement", if we implement those.
-fn safe_head<T: copy>(ls: @list<T>) : nonempty_list(ls) -> T {
-    check is_not_empty(ls);
+fn safe_head<T: copy>(ls: @list<T>) -> T {
+    assert is_not_empty(ls);
     ret head(ls);
 }
 
 fn main() {
     let mylist = @cons(@1u, @nil);
-    // Again, a way to eliminate such "obvious" checks seems
-    // desirable. (Tags could have postconditions.)
-    check (nonempty_list(mylist));
+    assert (nonempty_list(mylist));
     assert (*safe_head(mylist) == 1u);
 }
diff --git a/src/test/run-pass/pred-check.rs b/src/test/run-pass/pred-check.rs
deleted file mode 100644
index 588288cea2f..00000000000
--- a/src/test/run-pass/pred-check.rs
+++ /dev/null
@@ -1,4 +0,0 @@
-// -*- rust -*-
-pure fn f(q: int) -> bool { ret true; }
-
-fn main() { let x = 0; check (f(x)); }
diff --git a/src/test/run-pass/pred.rs b/src/test/run-pass/pred.rs
deleted file mode 100644
index 212e77cbdc1..00000000000
--- a/src/test/run-pass/pred.rs
+++ /dev/null
@@ -1,14 +0,0 @@
-// -*- rust -*-
-fn f(a: int, b: int) { }
-
-pure fn lt(a: int, b: int) -> bool { ret a < b; }
-
-fn main() {
-    let a: int = 10;
-    let b: int = 23;
-    let c: int = 77;
-    check (lt(a, b));
-    check (lt(a, c));
-    f(a, b);
-    f(a, c);
-}
diff --git a/src/test/run-pass/typestate-transitive.rs b/src/test/run-pass/typestate-transitive.rs
deleted file mode 100644
index 632aec5c4d1..00000000000
--- a/src/test/run-pass/typestate-transitive.rs
+++ /dev/null
@@ -1,7 +0,0 @@
-pure fn p(i: int) -> bool { true }
-
-fn f(i: int) : p(i) -> int { i }
-
-fn g(i: int) : p(i) -> int { f(i) }
-
-fn main() { }
diff --git a/src/test/run-pass/unchecked-predicates.rs b/src/test/run-pass/unchecked-predicates.rs
deleted file mode 100644
index c897c676329..00000000000
--- a/src/test/run-pass/unchecked-predicates.rs
+++ /dev/null
@@ -1,39 +0,0 @@
-// Uses foldl to exhibit the unchecked block syntax.
-use std;
-
-import std::list::*;
-
-// Can't easily be written as a "pure fn" because there's
-// no syntax for specifying that f is pure.
-fn pure_foldl<T: copy, U: copy>(ls: @list<T>, u: U, f: fn(T, U) -> U) -> U {
-    alt *ls {
-        nil { u }
-        cons(hd, tl) { f(hd, pure_foldl(tl, f(hd, u), f)) }
-    }
-}
-
-// Shows how to use an "unchecked" block to call a general
-// fn from a pure fn
-pure fn pure_length<T: copy>(ls: @list<T>) -> uint {
-    fn count<T>(_t: T, &&u: uint) -> uint { u + 1u }
-    unchecked{ pure_foldl(ls, 0u, count) }
-}
-
-pure fn nonempty_list<T: copy>(ls: @list<T>) -> bool { pure_length(ls) > 0u }
-
-// Of course, the compiler can't take advantage of the
-// knowledge that ls is a cons node. Future work.
-// Also, this is pretty contrived since nonempty_list
-// could be a "enum refinement", if we implement those.
-fn safe_head<T: copy>(ls: @list<T>) : nonempty_list(ls) -> T {
-    check is_not_empty(ls);
-    ret head(ls)
-}
-
-fn main() {
-    let mylist = @cons(@1u, @nil);
-    // Again, a way to eliminate such "obvious" checks seems
-    // desirable. (Tags could have postconditions.)
-    check (nonempty_list(mylist));
-    assert (*safe_head(mylist) == 1u);
-}
diff --git a/src/test/run-pass/weird-exprs.rs b/src/test/run-pass/weird-exprs.rs
index 27d45bde67d..104bea41e56 100644
--- a/src/test/run-pass/weird-exprs.rs
+++ b/src/test/run-pass/weird-exprs.rs
@@ -51,8 +51,8 @@ fn hammertime() -> int {
 
 fn canttouchthis() -> uint {
     pure fn p() -> bool { true }
-    let _a = (assert (true)) == (check (p()));
-    let _c = (check (p())) == ();
+    let _a = (assert (true)) == (assert (p()));
+    let _c = (assert (p())) == ();
     let _b: bool = (log(debug, 0) == (ret 0u));
 }
 
diff --git a/src/test/run-pass/zip-same-length.rs b/src/test/run-pass/zip-same-length.rs
index 13a50348469..3ae9f1c1eba 100644
--- a/src/test/run-pass/zip-same-length.rs
+++ b/src/test/run-pass/zip-same-length.rs
@@ -23,16 +23,11 @@ fn enum_uints(start: uint, end: uint) -> ~[uint] {
 
 fn main() {
     let a = 'a' as u8, j = 'j' as u8, k = 1u, l = 10u;
-    // Silly, but necessary
-    check (u8::le(a, j));
-    check (uint::le(k, l));
     let chars = enum_chars(a, j);
     let ints = enum_uints(k, l);
 
-    check (same_length(chars, ints));
     let ps = zip(chars, ints);
 
-    check (is_not_empty(ps));
     assert (head(ps) == ('a', 1u));
     assert (last(ps) == (j as char, 10u));
 }