diff --git a/Quantum.v b/Quantum.v
index 77006f2..b818491 100644
--- a/Quantum.v
+++ b/Quantum.v
@@ -1375,12 +1375,37 @@ Qed.
 Lemma braket0_hermitian : hermitian ∣0⟩⟨0∣. Proof. lma. Qed.
 Lemma braket1_hermitian : hermitian ∣1⟩⟨1∣. Proof. lma. Qed.
 
-
-#[global] Hint Rewrite hadamard_hermitian σx_hermitian σy_hermitian σz_hermitian cnot_hermitian swap_hermitian braket1_hermitian braket0_hermitian control_adjoint phase_adjoint rotation_adjoint : Q_db.
-
-
+(* Rewrite hangs on trying to rewrite hermitian, so we need to manually 
+   expose the underlying equality. This was the cause of a bad bug 
+   causing Qsimpl to hang. *)
+(* #[global] Hint Rewrite hadamard_hermitian σx_hermitian σy_hermitian σz_hermitian cnot_hermitian swap_hermitian braket1_hermitian braket0_hermitian control_adjoint phase_adjoint rotation_adjoint : Q_db. *)
+
+Local Ltac make_herm H :=
+  let T := type of H in 
+  let T' := eval unfold hermitian in T in 
+  exact (H : T').
+
+Definition hadamard_hermitian_rw := ltac:(make_herm hadamard_hermitian).
+Definition σx_hermitian_rw := ltac:(make_herm σx_hermitian).
+Definition σy_hermitian_rw := ltac:(make_herm σy_hermitian).
+Definition σz_hermitian_rw := ltac:(make_herm σz_hermitian).
+Definition cnot_hermitian_rw := ltac:(make_herm cnot_hermitian).
+Definition swap_hermitian_rw := ltac:(make_herm swap_hermitian).
+Definition braket1_hermitian_rw := ltac:(make_herm braket1_hermitian).
+Definition braket0_hermitian_rw := ltac:(make_herm braket0_hermitian).
+Definition control_adjoint_rw := ltac:(make_herm control_adjoint).
+Definition phase_adjoint_rw := ltac:(make_herm phase_adjoint).
+Definition rotation_adjoint_rw := ltac:(make_herm rotation_adjoint).
+
+
+#[global] Hint Rewrite hadamard_hermitian_rw 
+  σx_hermitian_rw σy_hermitian_rw σz_hermitian_rw cnot_hermitian_rw 
+  swap_hermitian_rw braket1_hermitian_rw braket0_hermitian_rw 
+  control_adjoint_rw phase_adjoint_rw rotation_adjoint_rw : Q_db.
 
 (* THESE ARE TO BE PHASED OUT *) 
+(* TODO: Is this true now that rewriting with 
+  hermitian is known to be impossible? *)
 
 
 
@@ -1475,7 +1500,6 @@ Lemma braqubit1_sa : ∣1⟩⟨1∣† = ∣1⟩⟨1∣. Proof. lma. Qed.
 
 *)
 
-#[global] Hint Rewrite hadamard_sa σx_sa σy_sa σz_sa cnot_sa swap_sa braqubit1_sa braqubit0_sa control_adjoint phase_adjoint rotation_adjoint : Q_db.
 
 (* Rather use control_adjoint :
 #[global] Hint Rewrite control_sa using (autorewrite with M_db; reflexivity) : M_db. *)
diff --git a/coq-quantumlib.opam b/coq-quantumlib.opam
index 23f69e4..98f6d97 100644
--- a/coq-quantumlib.opam
+++ b/coq-quantumlib.opam
@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "1.5.0"
+version: "1.5.1"
 synopsis: "Coq library for reasoning about quantum programs"
 description: """
 inQWIRE's QuantumLib is a Coq library for reasoning
diff --git a/dune-project b/dune-project
index 14c4cc4..7a9a3a6 100644
--- a/dune-project
+++ b/dune-project
@@ -1,6 +1,6 @@
 (lang dune 2.8)
 (name coq-quantumlib)
-(version 1.5.0)
+(version 1.5.1)
 (using coq 0.2)
 
 (generate_opam_files true)