From ffa450ba08590611db482f7618dc4fa48e08927d Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Wed, 10 Nov 2021 18:30:12 -0500
Subject: [PATCH] proof: normalize clauses in rw

---
 src/base/Proof_quip.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/base/Proof_quip.ml b/src/base/Proof_quip.ml
index 3078359c..18a75360 100644
--- a/src/base/Proof_quip.ml
+++ b/src/base/Proof_quip.ml
@@ -215,7 +215,7 @@ end = struct
           let name = name_clause lid in
 
           let step = lazy (
-            let c = L_proofs.find c in
+            let c = P.nn @@ L_proofs.find c in
             let using = Util.array_to_list_map L_proofs.find using in
             let res = !! res in
             P.S_step_c {name; res; proof=P.Clause_rw {res; c0=c; using}}