diff --git a/Cargo.toml b/Cargo.toml
index 18319430e..a60e13894 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -16,7 +16,7 @@ features = ["expose-arith"]
 rand = "0.3"
 blake2 = "0.7"
 digest = "0.7"
-bellman = "0.0.7"
+bellman = "0.0.8"
 
 [features]
 default = ["u128-support"]
diff --git a/src/circuit/blake2s.rs b/src/circuit/blake2s.rs
index 9a0d283ad..855a8c64f 100644
--- a/src/circuit/blake2s.rs
+++ b/src/circuit/blake2s.rs
@@ -90,13 +90,13 @@ const SIGMA: [[usize; 16]; 10] = [
 
 fn mixing_g<E: Engine, CS: ConstraintSystem<E>>(
     mut cs: CS,
-    v: &mut [UInt32<CS::Variable>],
+    v: &mut [UInt32],
     a: usize,
     b: usize,
     c: usize,
     d: usize,
-    x: &UInt32<CS::Variable>,
-    y: &UInt32<CS::Variable>
+    x: &UInt32,
+    y: &UInt32
 ) -> Result<(), SynthesisError>
 {
     v[a] = UInt32::addmany(cs.namespace(|| "mixing step 1"), &[v[a].clone(), v[b].clone(), x.clone()])?;
@@ -162,8 +162,8 @@ fn mixing_g<E: Engine, CS: ConstraintSystem<E>>(
 
 fn blake2s_compression<E: Engine, CS: ConstraintSystem<E>>(
     mut cs: CS,
-    h: &mut [UInt32<CS::Variable>],
-    m: &[UInt32<CS::Variable>],
+    h: &mut [UInt32],
+    m: &[UInt32],
     t: u64,
     f: bool
 ) -> Result<(), SynthesisError>
@@ -254,8 +254,8 @@ fn blake2s_compression<E: Engine, CS: ConstraintSystem<E>>(
 
 pub fn blake2s<E: Engine, CS: ConstraintSystem<E>>(
     mut cs: CS,
-    input: &[Boolean<CS::Variable>]
-) -> Result<Vec<Boolean<CS::Variable>>, SynthesisError>
+    input: &[Boolean]
+) -> Result<Vec<Boolean>, SynthesisError>
 {
     assert!(input.len() % 8 == 0);
 
@@ -269,7 +269,7 @@ pub fn blake2s<E: Engine, CS: ConstraintSystem<E>>(
     h.push(UInt32::constant(0x1F83D9AB));
     h.push(UInt32::constant(0x5BE0CD19));
 
-    let mut blocks: Vec<Vec<UInt32<CS::Variable>>> = vec![];
+    let mut blocks: Vec<Vec<UInt32>> = vec![];
 
     for block in input.chunks(512) {
         let mut this_block = Vec::with_capacity(16);
diff --git a/src/circuit/boolean.rs b/src/circuit/boolean.rs
index 6b5b9cd95..4d1c358a2 100644
--- a/src/circuit/boolean.rs
+++ b/src/circuit/boolean.rs
@@ -9,7 +9,8 @@ use pairing::{
 use bellman::{
     ConstraintSystem,
     SynthesisError,
-    LinearCombination
+    LinearCombination,
+    Variable
 };
 
 use super::{
@@ -19,17 +20,17 @@ use super::{
 /// Represents a variable in the constraint system which is guaranteed
 /// to be either zero or one.
 #[derive(Clone)]
-pub struct AllocatedBit<Var> {
-    variable: Var,
+pub struct AllocatedBit {
+    variable: Variable,
     value: Option<bool>
 }
 
-impl<Var: Copy> AllocatedBit<Var> {
+impl AllocatedBit {
     pub fn get_value(&self) -> Option<bool> {
         self.value
     }
 
-    pub fn get_variable(&self) -> Var {
+    pub fn get_variable(&self) -> Variable {
         self.variable
     }
 
@@ -40,7 +41,7 @@ impl<Var: Copy> AllocatedBit<Var> {
         value: Option<bool>,
     ) -> Result<Self, SynthesisError>
         where E: Engine,
-              CS: ConstraintSystem<E, Variable=Var>
+              CS: ConstraintSystem<E>
     {
         let var = cs.alloc(|| "boolean", || {
             if *value.get()? {
@@ -52,12 +53,11 @@ impl<Var: Copy> AllocatedBit<Var> {
 
         // Constrain: (1 - a) * a = 0
         // This constrains a to be either 0 or 1.
-        let one = cs.one();
         cs.enforce(
             || "boolean constraint",
-            LinearCombination::zero() + one - var,
-            LinearCombination::zero() + var,
-            LinearCombination::zero()
+            |lc| lc + CS::one() - var,
+            |lc| lc + var,
+            |lc| lc
         );
 
         Ok(AllocatedBit {
@@ -74,7 +74,7 @@ impl<Var: Copy> AllocatedBit<Var> {
         b: &Self
     ) -> Result<Self, SynthesisError>
         where E: Engine,
-              CS: ConstraintSystem<E, Variable=Var>
+              CS: ConstraintSystem<E>
     {
         let mut result_value = None;
 
@@ -107,9 +107,9 @@ impl<Var: Copy> AllocatedBit<Var> {
         // (a + a) * b = a + b - c
         cs.enforce(
             || "xor constraint",
-            LinearCombination::zero() + a.variable + a.variable,
-            LinearCombination::zero() + b.variable,
-            LinearCombination::zero() + a.variable + b.variable - result_var
+            |lc| lc + a.variable + a.variable,
+            |lc| lc + b.variable,
+            |lc| lc + a.variable + b.variable - result_var
         );
 
         Ok(AllocatedBit {
@@ -126,7 +126,7 @@ impl<Var: Copy> AllocatedBit<Var> {
         b: &Self
     ) -> Result<Self, SynthesisError>
         where E: Engine,
-              CS: ConstraintSystem<E, Variable=Var>
+              CS: ConstraintSystem<E>
     {
         let mut result_value = None;
 
@@ -146,9 +146,9 @@ impl<Var: Copy> AllocatedBit<Var> {
         // a AND b are both 1.
         cs.enforce(
             || "and constraint",
-            LinearCombination::zero() + a.variable,
-            LinearCombination::zero() + b.variable,
-            LinearCombination::zero() + result_var
+            |lc| lc + a.variable,
+            |lc| lc + b.variable,
+            |lc| lc + result_var
         );
 
         Ok(AllocatedBit {
@@ -164,7 +164,7 @@ impl<Var: Copy> AllocatedBit<Var> {
         b: &Self
     ) -> Result<Self, SynthesisError>
         where E: Engine,
-              CS: ConstraintSystem<E, Variable=Var>
+              CS: ConstraintSystem<E>
     {
         let mut result_value = None;
 
@@ -182,12 +182,11 @@ impl<Var: Copy> AllocatedBit<Var> {
 
         // Constrain (a) * (1 - b) = (c), ensuring c is 1 iff
         // a is true and b is false, and otherwise c is 0.
-        let one = cs.one();
         cs.enforce(
             || "and not constraint",
-            LinearCombination::zero() + a.variable,
-            LinearCombination::zero() + one - b.variable,
-            LinearCombination::zero() + result_var
+            |lc| lc + a.variable,
+            |lc| lc + CS::one() - b.variable,
+            |lc| lc + result_var
         );
 
         Ok(AllocatedBit {
@@ -203,7 +202,7 @@ impl<Var: Copy> AllocatedBit<Var> {
         b: &Self
     ) -> Result<Self, SynthesisError>
         where E: Engine,
-              CS: ConstraintSystem<E, Variable=Var>
+              CS: ConstraintSystem<E>
     {
         let mut result_value = None;
 
@@ -221,12 +220,11 @@ impl<Var: Copy> AllocatedBit<Var> {
 
         // Constrain (1 - a) * (1 - b) = (c), ensuring c is 1 iff
         // a and b are both false, and otherwise c is 0.
-        let one = cs.one();
         cs.enforce(
             || "nor constraint",
-            LinearCombination::zero() + one - a.variable,
-            LinearCombination::zero() + one - b.variable,
-            LinearCombination::zero() + result_var
+            |lc| lc + CS::one() - a.variable,
+            |lc| lc + CS::one() - b.variable,
+            |lc| lc + result_var
         );
 
         Ok(AllocatedBit {
@@ -239,23 +237,23 @@ impl<Var: Copy> AllocatedBit<Var> {
 /// This is a boolean value which may be either a constant or
 /// an interpretation of an `AllocatedBit`.
 #[derive(Clone)]
-pub enum Boolean<Var> {
+pub enum Boolean {
     /// Existential view of the boolean variable
-    Is(AllocatedBit<Var>),
+    Is(AllocatedBit),
     /// Negated view of the boolean variable
-    Not(AllocatedBit<Var>),
+    Not(AllocatedBit),
     /// Constant (not an allocated variable)
     Constant(bool)
 }
 
-impl<Var: Copy> Boolean<Var> {
+impl Boolean {
     pub fn enforce_equal<E, CS>(
         mut cs: CS,
         a: &Self,
         b: &Self
     ) -> Result<(), SynthesisError>
         where E: Engine,
-              CS: ConstraintSystem<E, Variable=Var>
+              CS: ConstraintSystem<E>
     {
         let c = Self::xor(&mut cs, a, b)?;
 
@@ -270,21 +268,25 @@ impl<Var: Copy> Boolean<Var> {
         }
     }
 
-    pub fn lc<E: Engine>(&self, one: Var, coeff: E::Fr) -> LinearCombination<Var, E>
+    pub fn lc<E: Engine>(
+        &self,
+        one: Variable,
+        coeff: E::Fr
+    ) -> LinearCombination<E>
     {
         match self {
             &Boolean::Constant(c) => {
                 if c {
-                    LinearCombination::<Var, E>::zero() + (coeff, one)
+                    LinearCombination::<E>::zero() + (coeff, one)
                 } else {
-                    LinearCombination::<Var, E>::zero()
+                    LinearCombination::<E>::zero()
                 }
             },
             &Boolean::Is(ref v) => {
-                LinearCombination::<Var, E>::zero() + (coeff, v.get_variable())
+                LinearCombination::<E>::zero() + (coeff, v.get_variable())
             },
             &Boolean::Not(ref v) => {
-                LinearCombination::<Var, E>::zero() + (coeff, one) - (coeff, v.get_variable())
+                LinearCombination::<E>::zero() + (coeff, one) - (coeff, v.get_variable())
             }
         }
     }
@@ -310,7 +312,7 @@ impl<Var: Copy> Boolean<Var> {
         b: &'a Self
     ) -> Result<Self, SynthesisError>
         where E: Engine,
-              CS: ConstraintSystem<E, Variable=Var>
+              CS: ConstraintSystem<E>
     {
         match (a, b) {
             (&Boolean::Constant(false), x) | (x, &Boolean::Constant(false)) => Ok(x.clone()),
@@ -337,7 +339,7 @@ impl<Var: Copy> Boolean<Var> {
         b: &'a Self
     ) -> Result<Self, SynthesisError>
         where E: Engine,
-              CS: ConstraintSystem<E, Variable=Var>
+              CS: ConstraintSystem<E>
     {
         match (a, b) {
             // false AND x is always false
@@ -364,7 +366,7 @@ impl<Var: Copy> Boolean<Var> {
         bits: &[Self]
     ) -> Result<Self, SynthesisError>
         where E: Engine,
-              CS: ConstraintSystem<E, Variable=Var>
+              CS: ConstraintSystem<E>
     {
         assert!(bits.len() > 0);
         let mut bits = bits.iter();
@@ -387,7 +389,7 @@ impl<Var: Copy> Boolean<Var> {
         bits: &[Self]
     ) -> Result<(), SynthesisError>
         where E: Engine,
-              CS: ConstraintSystem<E, Variable=Var>
+              CS: ConstraintSystem<E>
     {
         let res = Self::kary_and(&mut cs, bits)?;
 
@@ -396,25 +398,24 @@ impl<Var: Copy> Boolean<Var> {
                 Ok(())
             },
             Boolean::Constant(true) => {
-                Err(SynthesisError::AssignmentMissing)
+                Err(SynthesisError::Unsatisfiable)
             },
             Boolean::Is(ref res) => {
                 cs.enforce(
                     || "enforce nand",
-                    LinearCombination::zero(),
-                    LinearCombination::zero(),
-                    LinearCombination::zero() + res.get_variable()
+                    |lc| lc,
+                    |lc| lc,
+                    |lc| lc + res.get_variable()
                 );
 
                 Ok(())
             },
             Boolean::Not(ref res) => {
-                let one = cs.one();
                 cs.enforce(
                     || "enforce nand",
-                    LinearCombination::zero(),
-                    LinearCombination::zero(),
-                    LinearCombination::zero() + one - res.get_variable()
+                    |lc| lc,
+                    |lc| lc,
+                    |lc| lc + CS::one() - res.get_variable()
                 );
 
                 Ok(())
@@ -429,7 +430,7 @@ impl<Var: Copy> Boolean<Var> {
         bits: &[Self]
     ) -> Result<(), SynthesisError>
         where E: Engine,
-              CS: ConstraintSystem<E, Variable=Var>
+              CS: ConstraintSystem<E>
     {
         assert_eq!(bits.len(), F::NUM_BITS as usize);
 
@@ -440,7 +441,7 @@ impl<Var: Copy> Boolean<Var> {
         b.sub_noborrow(&1.into());
 
         // Runs of ones in r
-        let mut last_run = Boolean::<Var>::constant(true);
+        let mut last_run = Boolean::constant(true);
         let mut current_run = vec![];
 
         let mut found_one = false;
@@ -495,8 +496,8 @@ impl<Var: Copy> Boolean<Var> {
     }
 }
 
-impl<Var> From<AllocatedBit<Var>> for Boolean<Var> {
-    fn from(b: AllocatedBit<Var>) -> Boolean<Var> {
+impl From<AllocatedBit> for Boolean {
+    fn from(b: AllocatedBit) -> Boolean {
         Boolean::Is(b)
     }
 }
diff --git a/src/circuit/lookup.rs b/src/circuit/lookup.rs
index d44d5d36f..e433cd087 100644
--- a/src/circuit/lookup.rs
+++ b/src/circuit/lookup.rs
@@ -3,8 +3,7 @@ use super::*;
 use super::num::AllocatedNum;
 use super::boolean::Boolean;
 use bellman::{
-    ConstraintSystem,
-    LinearCombination
+    ConstraintSystem
 };
 
 // Synthesize the constants for each base pattern.
@@ -32,12 +31,12 @@ fn synth<'a, E: Engine, I>(
 
 /// Performs a 3-bit window table lookup. `bits` is in
 /// little-endian order.
-pub fn lookup3_xy<E: Engine, CS, Var: Copy>(
+pub fn lookup3_xy<E: Engine, CS>(
     mut cs: CS,
-    bits: &[Boolean<Var>],
+    bits: &[Boolean],
     coords: &[(E::Fr, E::Fr)]
-) -> Result<(AllocatedNum<E, Var>, AllocatedNum<E, Var>), SynthesisError>
-    where CS: ConstraintSystem<E, Variable=Var>
+) -> Result<(AllocatedNum<E>, AllocatedNum<E>), SynthesisError>
+    where CS: ConstraintSystem<E>
 {
     assert_eq!(bits.len(), 3);
     assert_eq!(coords.len(), 8);
@@ -85,34 +84,34 @@ pub fn lookup3_xy<E: Engine, CS, Var: Copy>(
 
     let precomp = Boolean::and(cs.namespace(|| "precomp"), &bits[1], &bits[2])?;
 
-    let one = cs.one();
+    let one = CS::one();
 
     cs.enforce(
         || "x-coordinate lookup",
-        LinearCombination::<Var, E>::zero() + (x_coeffs[0b001], one)
-                                            + &bits[1].lc::<E>(one, x_coeffs[0b011])
-                                            + &bits[2].lc::<E>(one, x_coeffs[0b101])
-                                            + &precomp.lc::<E>(one, x_coeffs[0b111]),
-        LinearCombination::<Var, E>::zero() + &bits[0].lc::<E>(one, E::Fr::one()),
-        LinearCombination::<Var, E>::zero() + res_x.get_variable()
-                                            - (x_coeffs[0b000], one)
-                                            - &bits[1].lc::<E>(one, x_coeffs[0b010])
-                                            - &bits[2].lc::<E>(one, x_coeffs[0b100])
-                                            - &precomp.lc::<E>(one, x_coeffs[0b110]),
+        |lc| lc + (x_coeffs[0b001], one)
+                + &bits[1].lc::<E>(one, x_coeffs[0b011])
+                + &bits[2].lc::<E>(one, x_coeffs[0b101])
+                + &precomp.lc::<E>(one, x_coeffs[0b111]),
+        |lc| lc + &bits[0].lc::<E>(one, E::Fr::one()),
+        |lc| lc + res_x.get_variable()
+                - (x_coeffs[0b000], one)
+                - &bits[1].lc::<E>(one, x_coeffs[0b010])
+                - &bits[2].lc::<E>(one, x_coeffs[0b100])
+                - &precomp.lc::<E>(one, x_coeffs[0b110]),
     );
 
     cs.enforce(
         || "y-coordinate lookup",
-        LinearCombination::<Var, E>::zero() + (y_coeffs[0b001], one)
-                                            + &bits[1].lc::<E>(one, y_coeffs[0b011])
-                                            + &bits[2].lc::<E>(one, y_coeffs[0b101])
-                                            + &precomp.lc::<E>(one, y_coeffs[0b111]),
-        LinearCombination::<Var, E>::zero() + &bits[0].lc::<E>(one, E::Fr::one()),
-        LinearCombination::<Var, E>::zero() + res_y.get_variable()
-                                            - (y_coeffs[0b000], one)
-                                            - &bits[1].lc::<E>(one, y_coeffs[0b010])
-                                            - &bits[2].lc::<E>(one, y_coeffs[0b100])
-                                            - &precomp.lc::<E>(one, y_coeffs[0b110]),
+        |lc| lc + (y_coeffs[0b001], one)
+                + &bits[1].lc::<E>(one, y_coeffs[0b011])
+                + &bits[2].lc::<E>(one, y_coeffs[0b101])
+                + &precomp.lc::<E>(one, y_coeffs[0b111]),
+        |lc| lc + &bits[0].lc::<E>(one, E::Fr::one()),
+        |lc| lc + res_y.get_variable()
+                - (y_coeffs[0b000], one)
+                - &bits[1].lc::<E>(one, y_coeffs[0b010])
+                - &bits[2].lc::<E>(one, y_coeffs[0b100])
+                - &precomp.lc::<E>(one, y_coeffs[0b110]),
     );
 
     Ok((res_x, res_y))
@@ -120,12 +119,12 @@ pub fn lookup3_xy<E: Engine, CS, Var: Copy>(
 
 /// Performs a 3-bit window table lookup, where
 /// one of the bits is a sign bit.
-pub fn lookup3_xy_with_conditional_negation<E: Engine, CS, Var: Copy>(
+pub fn lookup3_xy_with_conditional_negation<E: Engine, CS>(
     mut cs: CS,
-    bits: &[Boolean<Var>],
+    bits: &[Boolean],
     coords: &[(E::Fr, E::Fr)]
-) -> Result<(AllocatedNum<E, Var>, AllocatedNum<E, Var>), SynthesisError>
-    where CS: ConstraintSystem<E, Variable=Var>
+) -> Result<(AllocatedNum<E>, AllocatedNum<E>), SynthesisError>
+    where CS: ConstraintSystem<E>
 {
     assert_eq!(bits.len(), 3);
     assert_eq!(coords.len(), 4);
@@ -162,7 +161,7 @@ pub fn lookup3_xy_with_conditional_negation<E: Engine, CS, Var: Copy>(
         }
     )?;
 
-    let one = cs.one();
+    let one = CS::one();
 
     // Compute the coefficients for the lookup constraints
     let mut x_coeffs = [E::Fr::zero(); 4];
@@ -172,22 +171,22 @@ pub fn lookup3_xy_with_conditional_negation<E: Engine, CS, Var: Copy>(
 
     cs.enforce(
         || "x-coordinate lookup",
-        LinearCombination::<Var, E>::zero() + (x_coeffs[0b01], one)
-                                            + &bits[1].lc::<E>(one, x_coeffs[0b11]),
-        LinearCombination::<Var, E>::zero() + &bits[0].lc::<E>(one, E::Fr::one()),
-        LinearCombination::<Var, E>::zero() + res_x.get_variable()
-                                            - (x_coeffs[0b00], one)
-                                            - &bits[1].lc::<E>(one, x_coeffs[0b10])
+        |lc| lc + (x_coeffs[0b01], one)
+                + &bits[1].lc::<E>(one, x_coeffs[0b11]),
+        |lc| lc + &bits[0].lc::<E>(one, E::Fr::one()),
+        |lc| lc + res_x.get_variable()
+                - (x_coeffs[0b00], one)
+                - &bits[1].lc::<E>(one, x_coeffs[0b10])
     );
 
     cs.enforce(
         || "y-coordinate lookup",
-        LinearCombination::<Var, E>::zero() + (y_coeffs[0b01], one)
-                                            + &bits[1].lc::<E>(one, y_coeffs[0b11]),
-        LinearCombination::<Var, E>::zero() + &bits[0].lc::<E>(one, E::Fr::one()),
-        LinearCombination::<Var, E>::zero() + res_y.get_variable()
-                                            - (y_coeffs[0b00], one)
-                                            - &bits[1].lc::<E>(one, y_coeffs[0b10])
+        |lc| lc + (y_coeffs[0b01], one)
+                + &bits[1].lc::<E>(one, y_coeffs[0b11]),
+        |lc| lc + &bits[0].lc::<E>(one, E::Fr::one()),
+        |lc| lc + res_y.get_variable()
+                - (y_coeffs[0b00], one)
+                - &bits[1].lc::<E>(one, y_coeffs[0b10])
     );
 
     let final_y = res_y.conditionally_negate(&mut cs, &bits[2])?;
@@ -290,7 +289,7 @@ mod test {
 
         let window_size = 4;
 
-        let mut assignment = vec![Fr::zero(); (1 << window_size)];
+        let mut assignment = vec![Fr::zero(); 1 << window_size];
         let constants: Vec<_> = (0..(1 << window_size)).map(|_| Fr::rand(&mut rng)).collect();
 
         synth::<Bls12, _>(window_size, &constants, &mut assignment);
diff --git a/src/circuit/mod.rs b/src/circuit/mod.rs
index c36148704..45de18fd0 100644
--- a/src/circuit/mod.rs
+++ b/src/circuit/mod.rs
@@ -5,8 +5,8 @@ pub mod boolean;
 pub mod uint32;
 pub mod blake2s;
 pub mod num;
-pub mod mont;
 pub mod lookup;
+pub mod mont;
 pub mod pedersen_hash;
 
 use bellman::SynthesisError;
diff --git a/src/circuit/mont.rs b/src/circuit/mont.rs
index 0141c8ea7..81a2fcbee 100644
--- a/src/circuit/mont.rs
+++ b/src/circuit/mont.rs
@@ -5,8 +5,7 @@ use pairing::{
 
 use bellman::{
     SynthesisError,
-    ConstraintSystem,
-    LinearCombination
+    ConstraintSystem
 };
 
 use super::{
@@ -27,12 +26,12 @@ use super::lookup::{
 
 use super::boolean::Boolean;
 
-pub struct EdwardsPoint<E: Engine, Var> {
-    pub x: AllocatedNum<E, Var>,
-    pub y: AllocatedNum<E, Var>
+pub struct EdwardsPoint<E: Engine> {
+    pub x: AllocatedNum<E>,
+    pub y: AllocatedNum<E>
 }
 
-impl<E: Engine, Var: Copy> Clone for EdwardsPoint<E, Var> {
+impl<E: Engine> Clone for EdwardsPoint<E> {
     fn clone(&self) -> Self {
         EdwardsPoint {
             x: self.x.clone(),
@@ -44,15 +43,14 @@ impl<E: Engine, Var: Copy> Clone for EdwardsPoint<E, Var> {
 /// Perform a fixed-base scalar multiplication with
 /// `by` being in little-endian bit order. `by` must
 /// be a multiple of 3.
-pub fn fixed_base_multiplication<E, Var, CS>(
+pub fn fixed_base_multiplication<E, CS>(
     mut cs: CS,
     base: FixedGenerators,
-    by: &[Boolean<Var>],
+    by: &[Boolean],
     params: &E::Params
-) -> Result<EdwardsPoint<E, Var>, SynthesisError>
-    where CS: ConstraintSystem<E, Variable=Var>,
-          E: JubjubEngine,
-          Var: Copy
+) -> Result<EdwardsPoint<E>, SynthesisError>
+    where CS: ConstraintSystem<E>,
+          E: JubjubEngine
 {
     // We're going to chunk the scalar into 3-bit windows,
     // so let's force the caller to supply the right number
@@ -91,10 +89,10 @@ pub fn fixed_base_multiplication<E, Var, CS>(
     Ok(result.get()?.clone())
 }
 
-impl<E: JubjubEngine, Var: Copy> EdwardsPoint<E, Var> {
+impl<E: JubjubEngine> EdwardsPoint<E> {
     /// This extracts the x-coordinate, which is an injective
     /// encoding for elements of the prime order subgroup.
-    pub fn into_num(&self) -> AllocatedNum<E, Var> {
+    pub fn into_num(&self) -> AllocatedNum<E> {
         self.x.clone()
     }
 
@@ -103,9 +101,9 @@ impl<E: JubjubEngine, Var: Copy> EdwardsPoint<E, Var> {
     pub fn conditionally_select<CS>(
         &self,
         mut cs: CS,
-        condition: &Boolean<Var>
+        condition: &Boolean
     ) -> Result<Self, SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>
+        where CS: ConstraintSystem<E>
     {
         // Compute x' = self.x if condition, and 0 otherwise
         let x_prime = AllocatedNum::alloc(cs.namespace(|| "x'"), || {
@@ -119,12 +117,12 @@ impl<E: JubjubEngine, Var: Copy> EdwardsPoint<E, Var> {
         // condition * x = x'
         // if condition is 0, x' must be 0
         // if condition is 1, x' must be x
-        let one = cs.one();
+        let one = CS::one();
         cs.enforce(
             || "x' computation",
-            LinearCombination::<Var, E>::zero() + self.x.get_variable(),
-            condition.lc(one, E::Fr::one()),
-            LinearCombination::<Var, E>::zero() + x_prime.get_variable()
+            |lc| lc + self.x.get_variable(),
+            |_| condition.lc(one, E::Fr::one()),
+            |lc| lc + x_prime.get_variable()
         );
 
         // Compute y' = self.y if condition, and 1 otherwise
@@ -141,9 +139,9 @@ impl<E: JubjubEngine, Var: Copy> EdwardsPoint<E, Var> {
         // if condition is 1, y' must be y
         cs.enforce(
             || "y' computation",
-            LinearCombination::<Var, E>::zero() + self.y.get_variable(),
-            condition.lc(one, E::Fr::one()),
-            LinearCombination::<Var, E>::zero() + y_prime.get_variable()
+            |lc| lc + self.y.get_variable(),
+            |_| condition.lc(one, E::Fr::one()),
+            |lc| lc + y_prime.get_variable()
                                                 - &condition.not().lc(one, E::Fr::one())
         );
 
@@ -159,10 +157,10 @@ impl<E: JubjubEngine, Var: Copy> EdwardsPoint<E, Var> {
     pub fn mul<CS>(
         &self,
         mut cs: CS,
-        by: &[Boolean<Var>],
+        by: &[Boolean],
         params: &E::Params
     ) -> Result<Self, SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>
+        where CS: ConstraintSystem<E>
     {
         // Represents the current "magnitude" of the base
         // that we're operating over. Starts at self,
@@ -210,11 +208,11 @@ impl<E: JubjubEngine, Var: Copy> EdwardsPoint<E, Var> {
 
     pub fn interpret<CS>(
         mut cs: CS,
-        x: &AllocatedNum<E, Var>,
-        y: &AllocatedNum<E, Var>,
+        x: &AllocatedNum<E>,
+        y: &AllocatedNum<E>,
         params: &E::Params
     ) -> Result<Self, SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>
+        where CS: ConstraintSystem<E>
     {
         // -x^2 + y^2 = 1 + dx^2y^2
 
@@ -222,14 +220,14 @@ impl<E: JubjubEngine, Var: Copy> EdwardsPoint<E, Var> {
         let y2 = y.square(cs.namespace(|| "y^2"))?;
         let x2y2 = x2.mul(cs.namespace(|| "x^2 y^2"), &y2)?;
 
-        let one = cs.one();
+        let one = CS::one();
         cs.enforce(
             || "on curve check",
-            LinearCombination::zero() - x2.get_variable()
-                                      + y2.get_variable(),
-            LinearCombination::zero() + one,
-            LinearCombination::zero() + one
-                                      + (*params.edwards_d(), x2y2.get_variable())
+            |lc| lc - x2.get_variable()
+                    + y2.get_variable(),
+            |lc| lc + one,
+            |lc| lc + one
+                    + (*params.edwards_d(), x2y2.get_variable())
         );
 
         Ok(EdwardsPoint {
@@ -243,7 +241,7 @@ impl<E: JubjubEngine, Var: Copy> EdwardsPoint<E, Var> {
         cs: CS,
         params: &E::Params
     ) -> Result<Self, SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>
+        where CS: ConstraintSystem<E>
     {
         self.add(cs, self, params)
     }
@@ -255,7 +253,7 @@ impl<E: JubjubEngine, Var: Copy> EdwardsPoint<E, Var> {
         other: &Self,
         params: &E::Params
     ) -> Result<Self, SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>
+        where CS: ConstraintSystem<E>
     {
         // Compute U = (x1 + y1) * (x2 + y2)
         let u = AllocatedNum::alloc(cs.namespace(|| "U"), || {
@@ -272,11 +270,11 @@ impl<E: JubjubEngine, Var: Copy> EdwardsPoint<E, Var> {
 
         cs.enforce(
             || "U computation",
-            LinearCombination::<Var, E>::zero() + self.x.get_variable()
-                                                + self.y.get_variable(),
-            LinearCombination::<Var, E>::zero() + other.x.get_variable()
-                                                + other.y.get_variable(),
-            LinearCombination::<Var, E>::zero() + u.get_variable()
+            |lc| lc + self.x.get_variable()
+                    + self.y.get_variable(),
+            |lc| lc + other.x.get_variable()
+                    + other.y.get_variable(),
+            |lc| lc + u.get_variable()
         );
 
         // Compute A = y2 * x1
@@ -296,9 +294,9 @@ impl<E: JubjubEngine, Var: Copy> EdwardsPoint<E, Var> {
 
         cs.enforce(
             || "C computation",
-            LinearCombination::<Var, E>::zero() + (*params.edwards_d(), a.get_variable()),
-            LinearCombination::<Var, E>::zero() + b.get_variable(),
-            LinearCombination::<Var, E>::zero() + c.get_variable()
+            |lc| lc + (*params.edwards_d(), a.get_variable()),
+            |lc| lc + b.get_variable(),
+            |lc| lc + c.get_variable()
         );
 
         // Compute x3 = (A + B) / (1 + C)
@@ -316,18 +314,18 @@ impl<E: JubjubEngine, Var: Copy> EdwardsPoint<E, Var> {
                     Ok(t0)
                 },
                 None => {
-                    Err(SynthesisError::AssignmentMissing)
+                    Err(SynthesisError::DivisionByZero)
                 }
             }
         })?;
 
-        let one = cs.one();
+        let one = CS::one();
         cs.enforce(
             || "x3 computation",
-            LinearCombination::<Var, E>::zero() + one + c.get_variable(),
-            LinearCombination::<Var, E>::zero() + x3.get_variable(),
-            LinearCombination::<Var, E>::zero() + a.get_variable()
-                                                + b.get_variable()
+            |lc| lc + one + c.get_variable(),
+            |lc| lc + x3.get_variable(),
+            |lc| lc + a.get_variable()
+                    + b.get_variable()
         );
 
         // Compute y3 = (U - A - B) / (1 - C)
@@ -346,18 +344,18 @@ impl<E: JubjubEngine, Var: Copy> EdwardsPoint<E, Var> {
                     Ok(t0)
                 },
                 None => {
-                    Err(SynthesisError::AssignmentMissing)
+                    Err(SynthesisError::DivisionByZero)
                 }
             }
         })?;
 
         cs.enforce(
             || "y3 computation",
-            LinearCombination::<Var, E>::zero() + one - c.get_variable(),
-            LinearCombination::<Var, E>::zero() + y3.get_variable(),
-            LinearCombination::<Var, E>::zero() + u.get_variable()
-                                                - a.get_variable()
-                                                - b.get_variable()
+            |lc| lc + one - c.get_variable(),
+            |lc| lc + y3.get_variable(),
+            |lc| lc + u.get_variable()
+                    - a.get_variable()
+                    - b.get_variable()
         );
 
         Ok(EdwardsPoint {
@@ -367,12 +365,12 @@ impl<E: JubjubEngine, Var: Copy> EdwardsPoint<E, Var> {
     }
 }
 
-pub struct MontgomeryPoint<E: Engine, Var> {
-    x: AllocatedNum<E, Var>,
-    y: AllocatedNum<E, Var>
+pub struct MontgomeryPoint<E: Engine> {
+    x: AllocatedNum<E>,
+    y: AllocatedNum<E>
 }
 
-impl<E: JubjubEngine, Var: Copy> MontgomeryPoint<E, Var> {
+impl<E: JubjubEngine> MontgomeryPoint<E> {
     /// Converts an element in the prime order subgroup into
     /// a point in the birationally equivalent twisted
     /// Edwards curve.
@@ -380,8 +378,8 @@ impl<E: JubjubEngine, Var: Copy> MontgomeryPoint<E, Var> {
         &self,
         mut cs: CS,
         params: &E::Params
-    ) -> Result<EdwardsPoint<E, Var>, SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>
+    ) -> Result<EdwardsPoint<E>, SynthesisError>
+        where CS: ConstraintSystem<E>
     {
         // Compute u = (scale*x) / y
         let u = AllocatedNum::alloc(cs.namespace(|| "u"), || {
@@ -395,16 +393,16 @@ impl<E: JubjubEngine, Var: Copy> MontgomeryPoint<E, Var> {
                     Ok(t0)
                 },
                 None => {
-                    Err(SynthesisError::AssignmentMissing)
+                    Err(SynthesisError::DivisionByZero)
                 }
             }
         })?;
 
         cs.enforce(
             || "u computation",
-            LinearCombination::<Var, E>::zero() + self.y.get_variable(),
-            LinearCombination::<Var, E>::zero() + u.get_variable(),
-            LinearCombination::<Var, E>::zero() + (*params.scale(), self.x.get_variable())
+            |lc| lc + self.y.get_variable(),
+            |lc| lc + u.get_variable(),
+            |lc| lc + (*params.scale(), self.x.get_variable())
         );
 
         // Compute v = (x - 1) / (x + 1)
@@ -421,19 +419,19 @@ impl<E: JubjubEngine, Var: Copy> MontgomeryPoint<E, Var> {
                     Ok(t0)
                 },
                 None => {
-                    Err(SynthesisError::AssignmentMissing)
+                    Err(SynthesisError::DivisionByZero)
                 }
             }
         })?;
 
-        let one = cs.one();
+        let one = CS::one();
         cs.enforce(
             || "v computation",
-            LinearCombination::<Var, E>::zero() + self.x.get_variable()
-                                      + one,
-            LinearCombination::<Var, E>::zero() + v.get_variable(),
-            LinearCombination::<Var, E>::zero() + self.x.get_variable()
-                                      - one,
+            |lc| lc + self.x.get_variable()
+                    + one,
+            |lc| lc + v.get_variable(),
+            |lc| lc + self.x.get_variable()
+                    - one,
         );
 
         Ok(EdwardsPoint {
@@ -447,8 +445,8 @@ impl<E: JubjubEngine, Var: Copy> MontgomeryPoint<E, Var> {
     /// on the curve. Useful for constants and
     /// window table lookups.
     pub fn interpret_unchecked(
-        x: AllocatedNum<E, Var>,
-        y: AllocatedNum<E, Var>
+        x: AllocatedNum<E>,
+        y: AllocatedNum<E>
     ) -> Self
     {
         MontgomeryPoint {
@@ -465,7 +463,7 @@ impl<E: JubjubEngine, Var: Copy> MontgomeryPoint<E, Var> {
         other: &Self,
         params: &E::Params
     ) -> Result<Self, SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>
+        where CS: ConstraintSystem<E>
     {
         // Compute lambda = (y' - y) / (x' - x)
         let lambda = AllocatedNum::alloc(cs.namespace(|| "lambda"), || {
@@ -481,20 +479,20 @@ impl<E: JubjubEngine, Var: Copy> MontgomeryPoint<E, Var> {
                     Ok(n)
                 },
                 None => {
-                    Err(SynthesisError::AssignmentMissing)
+                    Err(SynthesisError::DivisionByZero)
                 }
             }
         })?;
 
         cs.enforce(
             || "evaluate lambda",
-            LinearCombination::<Var, E>::zero() + other.x.get_variable()
-                                                - self.x.get_variable(),
+            |lc| lc + other.x.get_variable()
+                    - self.x.get_variable(),
 
-            LinearCombination::zero()           + lambda.get_variable(),
+            |lc| lc + lambda.get_variable(),
 
-            LinearCombination::<Var, E>::zero() + other.y.get_variable()
-                                                - self.y.get_variable()
+            |lc| lc + other.y.get_variable()
+                    - self.y.get_variable()
         );
 
         // Compute x'' = lambda^2 - A - x - x'
@@ -509,15 +507,15 @@ impl<E: JubjubEngine, Var: Copy> MontgomeryPoint<E, Var> {
         })?;
 
         // (lambda) * (lambda) = (A + x + x' + x'')
-        let one = cs.one();
+        let one = CS::one();
         cs.enforce(
             || "evaluate xprime",
-            LinearCombination::zero()           + lambda.get_variable(),
-            LinearCombination::zero()           + lambda.get_variable(),
-            LinearCombination::<Var, E>::zero() + (*params.montgomery_a(), one)
-                                                + self.x.get_variable()
-                                                + other.x.get_variable()
-                                                + xprime.get_variable()
+            |lc| lc + lambda.get_variable(),
+            |lc| lc + lambda.get_variable(),
+            |lc| lc + (*params.montgomery_a(), one)
+                    + self.x.get_variable()
+                    + other.x.get_variable()
+                    + xprime.get_variable()
         );
 
         // Compute y' = -(y + lambda(x' - x))
@@ -534,13 +532,13 @@ impl<E: JubjubEngine, Var: Copy> MontgomeryPoint<E, Var> {
         // y' + y = lambda(x - x')
         cs.enforce(
             || "evaluate yprime",
-            LinearCombination::zero()           + self.x.get_variable()
-                                                - xprime.get_variable(),
+            |lc| lc + self.x.get_variable()
+                    - xprime.get_variable(),
 
-            LinearCombination::zero()           + lambda.get_variable(),
+            |lc| lc + lambda.get_variable(),
 
-            LinearCombination::<Var, E>::zero() + yprime.get_variable()
-                                                + self.y.get_variable()
+            |lc| lc + yprime.get_variable()
+                    + self.y.get_variable()
         );
 
         Ok(MontgomeryPoint {
@@ -556,7 +554,7 @@ impl<E: JubjubEngine, Var: Copy> MontgomeryPoint<E, Var> {
         mut cs: CS,
         params: &E::Params
     ) -> Result<Self, SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>
+        where CS: ConstraintSystem<E>
     {
         // Square x
         let xx = self.x.square(&mut cs)?;
@@ -580,25 +578,25 @@ impl<E: JubjubEngine, Var: Copy> MontgomeryPoint<E, Var> {
                     Ok(t0)
                 },
                 None => {
-                    Err(SynthesisError::AssignmentMissing)
+                    Err(SynthesisError::DivisionByZero)
                 }
             }
         })?;
 
         // (2.y) * (lambda) = (3.xx + 2.A.x + 1)
-        let one = cs.one();
+        let one = CS::one();
         cs.enforce(
             || "evaluate lambda",
-            LinearCombination::<Var, E>::zero() + self.y.get_variable()
-                                                + self.y.get_variable(),
+            |lc| lc + self.y.get_variable()
+                    + self.y.get_variable(),
 
-            LinearCombination::zero()           + lambda.get_variable(),
+            |lc| lc + lambda.get_variable(),
 
-            LinearCombination::<Var, E>::zero() + xx.get_variable()
-                                                + xx.get_variable()
-                                                + xx.get_variable()
-                                                + (*params.montgomery_2a(), self.x.get_variable())
-                                                + one
+            |lc| lc + xx.get_variable()
+                    + xx.get_variable()
+                    + xx.get_variable()
+                    + (*params.montgomery_2a(), self.x.get_variable())
+                    + one
         );
 
         // Compute x' = (lambda^2) - A - 2.x
@@ -615,12 +613,12 @@ impl<E: JubjubEngine, Var: Copy> MontgomeryPoint<E, Var> {
         // (lambda) * (lambda) = (A + 2.x + x')
         cs.enforce(
             || "evaluate xprime",
-            LinearCombination::zero()           + lambda.get_variable(),
-            LinearCombination::zero()           + lambda.get_variable(),
-            LinearCombination::<Var, E>::zero() + (*params.montgomery_a(), one)
-                                                + self.x.get_variable()
-                                                + self.x.get_variable()
-                                                + xprime.get_variable()
+            |lc| lc + lambda.get_variable(),
+            |lc| lc + lambda.get_variable(),
+            |lc| lc + (*params.montgomery_a(), one)
+                    + self.x.get_variable()
+                    + self.x.get_variable()
+                    + xprime.get_variable()
         );
 
         // Compute y' = -(y + lambda(x' - x))
@@ -637,13 +635,13 @@ impl<E: JubjubEngine, Var: Copy> MontgomeryPoint<E, Var> {
         // y' + y = lambda(x - x')
         cs.enforce(
             || "evaluate yprime",
-            LinearCombination::zero()           + self.x.get_variable()
-                                                - xprime.get_variable(),
+            |lc| lc + self.x.get_variable()
+                    - xprime.get_variable(),
 
-            LinearCombination::zero()           + lambda.get_variable(),
+            |lc| lc + lambda.get_variable(),
 
-            LinearCombination::<Var, E>::zero() + yprime.get_variable()
-                                                + self.y.get_variable()
+            |lc| lc + yprime.get_variable()
+                    + self.y.get_variable()
         );
 
         Ok(MontgomeryPoint {
diff --git a/src/circuit/num.rs b/src/circuit/num.rs
index 8656e4b7f..aca756276 100644
--- a/src/circuit/num.rs
+++ b/src/circuit/num.rs
@@ -8,7 +8,8 @@ use pairing::{
 use bellman::{
     SynthesisError,
     ConstraintSystem,
-    LinearCombination
+    LinearCombination,
+    Variable
 };
 
 use super::{
@@ -20,12 +21,12 @@ use super::boolean::{
    AllocatedBit
 };
 
-pub struct AllocatedNum<E: Engine, Var> {
+pub struct AllocatedNum<E: Engine> {
     value: Option<E::Fr>,
-    variable: Var
+    variable: Variable
 }
 
-impl<Var: Copy, E: Engine> Clone for AllocatedNum<E, Var> {
+impl<E: Engine> Clone for AllocatedNum<E> {
     fn clone(&self) -> Self {
         AllocatedNum {
             value: self.value,
@@ -34,12 +35,12 @@ impl<Var: Copy, E: Engine> Clone for AllocatedNum<E, Var> {
     }
 }
 
-impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
+impl<E: Engine> AllocatedNum<E> {
     pub fn alloc<CS, F>(
         mut cs: CS,
         value: F,
     ) -> Result<Self, SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>,
+        where CS: ConstraintSystem<E>,
               F: FnOnce() -> Result<E::Fr, SynthesisError>
     {
         let mut new_value = None;
@@ -60,8 +61,8 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
     pub fn into_bits_strict<CS>(
         &self,
         mut cs: CS
-    ) -> Result<Vec<Boolean<Var>>, SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>
+    ) -> Result<Vec<Boolean>, SynthesisError>
+        where CS: ConstraintSystem<E>
     {
         let bits = self.into_bits(&mut cs)?;
         Boolean::enforce_in_field::<_, _, E::Fr>(&mut cs, &bits)?;
@@ -72,8 +73,8 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
     pub fn into_bits<CS>(
         &self,
         mut cs: CS
-    ) -> Result<Vec<Boolean<Var>>, SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>
+    ) -> Result<Vec<Boolean>, SynthesisError>
+        where CS: ConstraintSystem<E>
     {
         let bit_values = match self.value {
             Some(value) => {
@@ -122,9 +123,9 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
 
         cs.enforce(
             || "unpacking constraint",
-            LinearCombination::zero(),
-            LinearCombination::zero(),
-            lc
+            |lc| lc,
+            |lc| lc,
+            |_| lc
         );
 
         Ok(bits.into_iter().map(|b| Boolean::from(b)).collect())
@@ -132,16 +133,16 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
 
     pub fn from_bits_strict<CS>(
         mut cs: CS,
-        bits: &[Boolean<Var>]
+        bits: &[Boolean]
     ) -> Result<Self, SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>
+        where CS: ConstraintSystem<E>
     {
         assert_eq!(bits.len(), E::Fr::NUM_BITS as usize);
 
         Boolean::enforce_in_field::<_, _, E::Fr>(&mut cs, bits)?;
 
-        let one = cs.one();
-        let mut lc = LinearCombination::<Var, E>::zero();
+        let one = CS::one();
+        let mut lc = LinearCombination::<E>::zero();
         let mut coeff = E::Fr::one();
         let mut value = Some(E::Fr::zero());
         for bit in bits.iter().rev() {
@@ -191,9 +192,9 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
 
         cs.enforce(
             || "packing constraint",
-            LinearCombination::zero(),
-            LinearCombination::zero(),
-            lc
+            |lc| lc,
+            |lc| lc,
+            |_| lc
         );
 
         Ok(num)
@@ -204,7 +205,7 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
         mut cs: CS,
         other: &Self
     ) -> Result<Self, SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>
+        where CS: ConstraintSystem<E>
     {
         let mut value = None;
 
@@ -220,9 +221,9 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
         // Constrain: a * b = ab
         cs.enforce(
             || "multiplication constraint",
-            LinearCombination::zero() + self.variable,
-            LinearCombination::zero() + other.variable,
-            LinearCombination::zero() + var
+            |lc| lc + self.variable,
+            |lc| lc + other.variable,
+            |lc| lc + var
         );
 
         Ok(AllocatedNum {
@@ -235,7 +236,7 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
         &self,
         mut cs: CS
     ) -> Result<Self, SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>
+        where CS: ConstraintSystem<E>
     {
         let mut value = None;
 
@@ -251,9 +252,9 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
         // Constrain: a * a = aa
         cs.enforce(
             || "squaring constraint",
-            LinearCombination::zero() + self.variable,
-            LinearCombination::zero() + self.variable,
-            LinearCombination::zero() + var
+            |lc| lc + self.variable,
+            |lc| lc + self.variable,
+            |lc| lc + var
         );
 
         Ok(AllocatedNum {
@@ -266,13 +267,13 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
         &self,
         mut cs: CS
     ) -> Result<(), SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>
+        where CS: ConstraintSystem<E>
     {
         let inv = cs.alloc(|| "ephemeral inverse", || {
             let tmp = *self.value.get()?;
             
             if tmp.is_zero() {
-                Err(SynthesisError::AssignmentMissing)
+                Err(SynthesisError::DivisionByZero)
             } else {
                 Ok(tmp.inverse().unwrap())
             }
@@ -281,12 +282,11 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
         // Constrain a * inv = 1, which is only valid
         // iff a has a multiplicative inverse, untrue
         // for zero.
-        let one = cs.one();
         cs.enforce(
             || "nonzero assertion constraint",
-            LinearCombination::zero() + self.variable,
-            LinearCombination::zero() + inv,
-            LinearCombination::zero() + one
+            |lc| lc + self.variable,
+            |lc| lc + inv,
+            |lc| lc + CS::one()
         );
 
         Ok(())
@@ -299,9 +299,9 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
         mut cs: CS,
         a: &Self,
         b: &Self,
-        condition: &Boolean<Var>
+        condition: &Boolean
     ) -> Result<(Self, Self), SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>
+        where CS: ConstraintSystem<E>
     {
         let c = Self::alloc(
             cs.namespace(|| "conditional reversal result 1"),
@@ -314,12 +314,11 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
             }
         )?;
 
-        let one = cs.one();
         cs.enforce(
             || "first conditional reversal",
-            LinearCombination::zero() + a.variable - b.variable,
-            condition.lc(one, E::Fr::one()),
-            LinearCombination::zero() + a.variable - c.variable
+            |lc| lc + a.variable - b.variable,
+            |_| condition.lc(CS::one(), E::Fr::one()),
+            |lc| lc + a.variable - c.variable
         );
 
         let d = Self::alloc(
@@ -335,9 +334,9 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
 
         cs.enforce(
             || "second conditional reversal",
-            LinearCombination::zero() + b.variable - a.variable,
-            condition.lc(one, E::Fr::one()),
-            LinearCombination::zero() + b.variable - d.variable
+            |lc| lc + b.variable - a.variable,
+            |_| condition.lc(CS::one(), E::Fr::one()),
+            |lc| lc + b.variable - d.variable
         );
 
         Ok((c, d))
@@ -346,9 +345,9 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
     pub fn conditionally_negate<CS>(
         &self,
         mut cs: CS,
-        condition: &Boolean<Var>
+        condition: &Boolean
     ) -> Result<Self, SynthesisError>
-        where CS: ConstraintSystem<E, Variable=Var>
+        where CS: ConstraintSystem<E>
     {
         let r = Self::alloc(
             cs.namespace(|| "conditional negation result"),
@@ -365,12 +364,11 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
         // x - 2cx = r
         // (2x) * (c) = x - r
 
-        let one = cs.one();
         cs.enforce(
             || "conditional negation",
-            LinearCombination::zero() + self.variable + self.variable,
-            condition.lc(one, E::Fr::one()),
-            LinearCombination::zero() + self.variable - r.variable
+            |lc| lc + self.variable + self.variable,
+            |_| condition.lc(CS::one(), E::Fr::one()),
+            |lc| lc + self.variable - r.variable
         );
 
         Ok(r)
@@ -380,7 +378,7 @@ impl<E: Engine, Var: Copy> AllocatedNum<E, Var> {
         self.value
     }
 
-    pub fn get_variable(&self) -> Var {
+    pub fn get_variable(&self) -> Variable {
         self.variable
     }
 }
diff --git a/src/circuit/pedersen_hash.rs b/src/circuit/pedersen_hash.rs
index ee940a382..a405b7a45 100644
--- a/src/circuit/pedersen_hash.rs
+++ b/src/circuit/pedersen_hash.rs
@@ -10,12 +10,12 @@ use bellman::{
 };
 use super::lookup::*;
 
-pub fn pedersen_hash<E: JubjubEngine, CS, Var: Copy>(
+pub fn pedersen_hash<E: JubjubEngine, CS>(
     mut cs: CS,
-    bits: &[Boolean<Var>],
+    bits: &[Boolean],
     params: &E::Params
-) -> Result<EdwardsPoint<E, Var>, SynthesisError>
-    where CS: ConstraintSystem<E, Variable=Var>
+) -> Result<EdwardsPoint<E>, SynthesisError>
+    where CS: ConstraintSystem<E>
 {
     // Unnecessary if forced personalization is introduced
     assert!(bits.len() > 0);
@@ -116,7 +116,7 @@ mod test {
 
         let input: Vec<bool> = (0..(Fr::NUM_BITS * 2)).map(|_| rng.gen()).collect();
 
-        let input_bools: Vec<Boolean<_>> = input.iter().enumerate().map(|(i, b)| {
+        let input_bools: Vec<Boolean> = input.iter().enumerate().map(|(i, b)| {
             Boolean::from(
                 AllocatedBit::alloc(cs.namespace(|| format!("input {}", i)), Some(*b)).unwrap()
             )
@@ -143,7 +143,7 @@ mod test {
 
                 let mut cs = TestConstraintSystem::<Bls12>::new();
 
-                let input_bools: Vec<Boolean<_>> = input.iter().enumerate().map(|(i, b)| {
+                let input_bools: Vec<Boolean> = input.iter().enumerate().map(|(i, b)| {
                     Boolean::from(
                         AllocatedBit::alloc(cs.namespace(|| format!("input {}", i)), Some(*b)).unwrap()
                     )
diff --git a/src/circuit/test/mod.rs b/src/circuit/test/mod.rs
index 22575e93e..ef042fe62 100644
--- a/src/circuit/test/mod.rs
+++ b/src/circuit/test/mod.rs
@@ -6,17 +6,13 @@ use pairing::{
 use bellman::{
     LinearCombination,
     SynthesisError,
-    ConstraintSystem
+    ConstraintSystem,
+    Variable,
+    Index
 };
 
 use std::collections::HashMap;
 
-#[derive(Debug, Copy, Clone)]
-pub enum Variable {
-    Input(usize),
-    Aux(usize)
-}
-
 #[derive(Debug)]
 enum NamedObject {
     Constraint(usize),
@@ -28,7 +24,12 @@ enum NamedObject {
 pub struct TestConstraintSystem<E: Engine> {
     named_objects: HashMap<String, NamedObject>,
     current_namespace: Vec<String>,
-    constraints: Vec<(LinearCombination<Variable, E>, LinearCombination<Variable, E>, LinearCombination<Variable, E>, String)>,
+    constraints: Vec<(
+        LinearCombination<E>,
+        LinearCombination<E>,
+        LinearCombination<E>,
+        String
+    )>,
     inputs: Vec<(E::Fr, String)>,
     aux: Vec<(E::Fr, String)>
 }
@@ -42,9 +43,9 @@ fn eval_lc<E: Engine>(
     let mut acc = E::Fr::zero();
 
     for &(var, ref coeff) in terms {
-        let mut tmp = match var {
-            Variable::Input(index) => inputs[index].0,
-            Variable::Aux(index) => aux[index].0
+        let mut tmp = match var.get_unchecked() {
+            Index::Input(index) => inputs[index].0,
+            Index::Aux(index) => aux[index].0
         };
 
         tmp.mul_assign(&coeff);
@@ -57,7 +58,7 @@ fn eval_lc<E: Engine>(
 impl<E: Engine> TestConstraintSystem<E> {
     pub fn new() -> TestConstraintSystem<E> {
         let mut map = HashMap::new();
-        map.insert("ONE".into(), NamedObject::Var(Variable::Input(0)));
+        map.insert("ONE".into(), NamedObject::Var(TestConstraintSystem::<E>::one()));
 
         TestConstraintSystem {
             named_objects: map,
@@ -97,8 +98,12 @@ impl<E: Engine> TestConstraintSystem<E> {
     pub fn set(&mut self, path: &str, to: E::Fr)
     {
         match self.named_objects.get(path) {
-            Some(&NamedObject::Var(Variable::Input(index))) => self.inputs[index].0 = to,
-            Some(&NamedObject::Var(Variable::Aux(index))) => self.aux[index].0 = to,
+            Some(&NamedObject::Var(ref v)) => {
+                match v.get_unchecked() {
+                    Index::Input(index) => self.inputs[index].0 = to,
+                    Index::Aux(index) => self.aux[index].0 = to
+                }
+            }
             Some(e) => panic!("tried to set path `{}` to value, but `{:?}` already exists there.", path, e),
             _ => panic!("no variable exists at path: {}", path)
         }
@@ -107,8 +112,12 @@ impl<E: Engine> TestConstraintSystem<E> {
     pub fn get(&mut self, path: &str) -> E::Fr
     {
         match self.named_objects.get(path) {
-            Some(&NamedObject::Var(Variable::Input(index))) => self.inputs[index].0,
-            Some(&NamedObject::Var(Variable::Aux(index))) => self.aux[index].0,
+            Some(&NamedObject::Var(ref v)) => {
+                match v.get_unchecked() {
+                    Index::Input(index) => self.inputs[index].0,
+                    Index::Aux(index) => self.aux[index].0
+                }
+            }
             Some(e) => panic!("tried to get value of path `{}`, but `{:?}` exists there (not a variable)", path, e),
             _ => panic!("no variable exists at path: {}", path)
         }
@@ -145,42 +154,60 @@ fn compute_path(ns: &[String], this: String) -> String {
 }
 
 impl<E: Engine> ConstraintSystem<E> for TestConstraintSystem<E> {
-    type Variable = Variable;
     type Root = Self;
 
-    fn one(&self) -> Self::Variable {
-        Variable::Input(0)
-    }
-
     fn alloc<F, A, AR>(
         &mut self,
         annotation: A,
         f: F
-    ) -> Result<Self::Variable, SynthesisError>
+    ) -> Result<Variable, SynthesisError>
         where F: FnOnce() -> Result<E::Fr, SynthesisError>, A: FnOnce() -> AR, AR: Into<String>
     {
         let index = self.aux.len();
         let path = compute_path(&self.current_namespace, annotation().into());
         self.aux.push((f()?, path.clone()));
-        let var = Variable::Aux(index);
+        let var = Variable::new_unchecked(Index::Aux(index));
         self.set_named_obj(path, NamedObject::Var(var));
 
         Ok(var)
     }
 
-    fn enforce<A, AR>(
+    fn alloc_input<F, A, AR>(
         &mut self,
         annotation: A,
-        a: LinearCombination<Self::Variable, E>,
-        b: LinearCombination<Self::Variable, E>,
-        c: LinearCombination<Self::Variable, E>
+        f: F
+    ) -> Result<Variable, SynthesisError>
+        where F: FnOnce() -> Result<E::Fr, SynthesisError>, A: FnOnce() -> AR, AR: Into<String>
+    {
+        let index = self.inputs.len();
+        let path = compute_path(&self.current_namespace, annotation().into());
+        self.inputs.push((f()?, path.clone()));
+        let var = Variable::new_unchecked(Index::Input(index));
+        self.set_named_obj(path, NamedObject::Var(var));
+
+        Ok(var)
+    }
+
+    fn enforce<A, AR, LA, LB, LC>(
+        &mut self,
+        annotation: A,
+        a: LA,
+        b: LB,
+        c: LC
     )
-        where A: FnOnce() -> AR, AR: Into<String>
+        where A: FnOnce() -> AR, AR: Into<String>,
+              LA: FnOnce(LinearCombination<E>) -> LinearCombination<E>,
+              LB: FnOnce(LinearCombination<E>) -> LinearCombination<E>,
+              LC: FnOnce(LinearCombination<E>) -> LinearCombination<E>
     {
         let path = compute_path(&self.current_namespace, annotation().into());
         let index = self.constraints.len();
         self.set_named_obj(path.clone(), NamedObject::Constraint(index));
 
+        let a = a(LinearCombination::zero());
+        let b = b(LinearCombination::zero());
+        let c = c(LinearCombination::zero());
+
         self.constraints.push((a, b, c, path));
     }
 
@@ -218,21 +245,21 @@ fn test_cs() {
 
     cs.enforce(
         || "mult",
-        LinearCombination::zero() + a,
-        LinearCombination::zero() + b,
-        LinearCombination::zero() + c
+        |lc| lc + a,
+        |lc| lc + b,
+        |lc| lc + c
     );
     assert!(cs.is_satisfied());
     assert_eq!(cs.num_constraints(), 1);
 
     cs.set("a/var", Fr::from_str("4").unwrap());
 
-    let one = cs.one();
+    let one = TestConstraintSystem::<Bls12>::one();
     cs.enforce(
         || "eq",
-        LinearCombination::zero() + a,
-        LinearCombination::zero() + one,
-        LinearCombination::zero() + b
+        |lc| lc + a,
+        |lc| lc + one,
+        |lc| lc + b
     );
 
     assert!(!cs.is_satisfied());
diff --git a/src/circuit/uint32.rs b/src/circuit/uint32.rs
index 7f93879da..ff3943377 100644
--- a/src/circuit/uint32.rs
+++ b/src/circuit/uint32.rs
@@ -18,13 +18,13 @@ use super::boolean::{
 /// Represents an interpretation of 32 `Boolean` objects as an
 /// unsigned integer.
 #[derive(Clone)]
-pub struct UInt32<Var> {
+pub struct UInt32 {
     // Least significant bit first
-    bits: Vec<Boolean<Var>>,
+    bits: Vec<Boolean>,
     value: Option<u32>
 }
 
-impl<Var: Copy> UInt32<Var> {
+impl UInt32 {
     /// Construct a constant `UInt32` from a `u32`
     pub fn constant(value: u32) -> Self
     {
@@ -53,7 +53,7 @@ impl<Var: Copy> UInt32<Var> {
         value: Option<u32>
     ) -> Result<Self, SynthesisError>
         where E: Engine,
-              CS: ConstraintSystem<E, Variable=Var>
+              CS: ConstraintSystem<E>
     {
         let values = match value {
             Some(mut val) => {
@@ -72,7 +72,10 @@ impl<Var: Copy> UInt32<Var> {
         let bits = values.into_iter()
                          .enumerate()
                          .map(|(i, v)| {
-                            Ok(Boolean::from(AllocatedBit::alloc(cs.namespace(|| format!("allocated bit {}", i)), v)?))
+                            Ok(Boolean::from(AllocatedBit::alloc(
+                                cs.namespace(|| format!("allocated bit {}", i)),
+                                v
+                            )?))
                          })
                          .collect::<Result<Vec<_>, SynthesisError>>()?;
 
@@ -83,7 +86,7 @@ impl<Var: Copy> UInt32<Var> {
     }
 
     /// Turns this `UInt32` into its little-endian byte order representation.
-    pub fn into_bits(&self) -> Vec<Boolean<Var>> {
+    pub fn into_bits(&self) -> Vec<Boolean> {
         self.bits.chunks(8)
                  .flat_map(|v| v.iter().rev())
                  .cloned()
@@ -92,7 +95,7 @@ impl<Var: Copy> UInt32<Var> {
 
     /// Converts a little-endian byte order representation of bits into a
     /// `UInt32`.
-    pub fn from_bits(bits: &[Boolean<Var>]) -> Self
+    pub fn from_bits(bits: &[Boolean]) -> Self
     {
         assert_eq!(bits.len(), 32);
 
@@ -157,7 +160,7 @@ impl<Var: Copy> UInt32<Var> {
         other: &Self
     ) -> Result<Self, SynthesisError>
         where E: Engine,
-              CS: ConstraintSystem<E, Variable=Var>
+              CS: ConstraintSystem<E>
     {
         let new_value = match (self.value, other.value) {
             (Some(a), Some(b)) => {
@@ -170,7 +173,11 @@ impl<Var: Copy> UInt32<Var> {
                             .zip(other.bits.iter())
                             .enumerate()
                             .map(|(i, (a, b))| {
-                                Boolean::xor(cs.namespace(|| format!("xor of bit {}", i)), a, b)
+                                Boolean::xor(
+                                    cs.namespace(|| format!("xor of bit {}", i)),
+                                    a,
+                                    b
+                                )
                             })
                             .collect::<Result<_, _>>()?;
 
@@ -186,7 +193,7 @@ impl<Var: Copy> UInt32<Var> {
         operands: &[Self]
     ) -> Result<Self, SynthesisError>
         where E: Engine,
-              CS: ConstraintSystem<E, Variable=Var>
+              CS: ConstraintSystem<E>
     {
         // Make some arbitrary bounds for ourselves to avoid overflows
         // in the scalar field
@@ -235,11 +242,11 @@ impl<Var: Copy> UInt32<Var> {
                         all_constants = false;
 
                         // Add coeff * (1 - bit) = coeff * ONE - coeff * bit
-                        lc = lc + (coeff, cs.one()) - (coeff, bit.get_variable());
+                        lc = lc + (coeff, CS::one()) - (coeff, bit.get_variable());
                     },
                     &Boolean::Constant(bit) => {
                         if bit {
-                            lc = lc + (coeff, cs.one());
+                            lc = lc + (coeff, CS::one());
                         }
                     }
                 }
@@ -266,7 +273,10 @@ impl<Var: Copy> UInt32<Var> {
         let mut i = 0;
         while max_value != 0 {
             // Allocate the bit
-            let b = AllocatedBit::alloc(cs.namespace(|| format!("result bit {}", i)), result_value.map(|v| (v >> i) & 1 == 1))?;
+            let b = AllocatedBit::alloc(
+                cs.namespace(|| format!("result bit {}", i)),
+                result_value.map(|v| (v >> i) & 1 == 1)
+            )?;
 
             // Subtract this bit from the linear combination to ensure the sums balance out
             lc = lc - (coeff, b.get_variable());
@@ -281,9 +291,9 @@ impl<Var: Copy> UInt32<Var> {
         // Enforce that the linear combination equals zero
         cs.enforce(
             || "modular addition",
-            LinearCombination::zero(),
-            LinearCombination::zero(),
-            lc
+            |lc| lc,
+            |lc| lc,
+            |_| lc
         );
 
         // Discard carry bits that we don't care about
@@ -311,7 +321,7 @@ mod test {
         let mut rng = XorShiftRng::from_seed([0x5dbe6259, 0x8d313d76, 0x3237db17, 0xe5bc0653]);
 
         for _ in 0..1000 {
-            let mut v = (0..32).map(|_| Boolean::<()>::constant(rng.gen())).collect::<Vec<_>>();
+            let mut v = (0..32).map(|_| Boolean::constant(rng.gen())).collect::<Vec<_>>();
 
             let b = UInt32::from_bits(&v);
 
@@ -473,7 +483,7 @@ mod test {
 
         let mut num = rng.gen();
 
-        let a = UInt32::<()>::constant(num);
+        let a = UInt32::constant(num);
 
         for i in 0..32 {
             let b = a.rotr(i);