From 0d00629923e08ccbe5d359cab8d0807e5d449144 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Wed, 10 Nov 2021 13:23:29 -0500
Subject: [PATCH] more compressed output of equations

---
 src/base/Proof_quip.ml | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/src/base/Proof_quip.ml b/src/base/Proof_quip.ml
index eff76e3a..1cc9e47d 100644
--- a/src/base/Proof_quip.ml
+++ b/src/base/Proof_quip.ml
@@ -130,12 +130,15 @@ end = struct
         | PS.Step_view.Expr_eq { lhs; rhs } ->
           add_needed_step lhs;
           add_needed_step rhs;
-          let t = lazy (
+          let name = name_term lid in
+          let step = lazy (
             let lhs = L_terms.find lhs
             and rhs = L_terms.find rhs in
-            P.T.eq lhs rhs
+            let t = P.T.eq lhs rhs in
+            P.S_define_t_name (name, t)
           ) in
-          L_terms.add lid t
+          add_top_step step;
+          L_terms.add lid (lazy (P.T.ref name))
 
         | PS.Step_view.Expr_bool {b} ->
           let t = Lazy.from_val (P.T.bool b) in