diff --git a/src/Lean/Elab/Tactic/Calc.lean b/src/Lean/Elab/Tactic/Calc.lean
index 65f24ff9c5..4a704209f7 100644
--- a/src/Lean/Elab/Tactic/Calc.lean
+++ b/src/Lean/Elab/Tactic/Calc.lean
@@ -18,7 +18,7 @@ def elabCalcSteps (steps : Array Syntax) : TacticM Expr := do
 where
   go : TermElabM Expr := do
     let e ← Term.elabCalcSteps steps
-    Term.synthesizeSyntheticMVars
+    Term.synthesizeSyntheticMVars (mayPostpone := false)
     instantiateMVars e
 
 @[builtinTactic calcTactic]
diff --git a/tests/lean/run/1372.lean b/tests/lean/run/1372.lean
new file mode 100644
index 0000000000..634521784a
--- /dev/null
+++ b/tests/lean/run/1372.lean
@@ -0,0 +1,16 @@
+example (x₁ x₂ y₁ y₂ : Nat) : (x₁ + x₂) + (y₁ + y₂) = (x₁ + y₁) + (x₂ + y₂) := by
+  calc (x₁ + x₂) + (y₁ + y₂)
+      = x₁ + (x₂ + (y₁ + y₂)) := by rw [Nat.add_assoc]
+    _ = x₁ + (y₁ + (x₂ + y₂)) := by rw [Nat.add_left_comm x₂ y₁ y₂]
+    _ = (x₁ + y₁) + (x₂ + y₂) := by rw [Nat.add_assoc]
+
+
+example (n x₁ x₂ y₁ y₂ : Nat) : n = 0 → (x₁ + x₂) + (y₁ + y₂) = (x₁ + y₁) + (x₂ + y₂) := by
+  intro h
+  induction n with
+  | zero =>
+    calc (x₁ + x₂) + (y₁ + y₂)
+       = x₁ + (x₂ + (y₁ + y₂)) := by rw [Nat.add_assoc]
+     _ = x₁ + (y₁ + (x₂ + y₂)) := by rw [Nat.add_left_comm x₂ y₁ y₂]
+     _ = (x₁ + y₁) + (x₂ + y₂) := by rw [Nat.add_assoc]
+  | succ _ _ => contradiction