From ca58a8015646158fae415ef4b3edc350d6eaefbc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 19 Aug 2020 17:33:30 +0200
Subject: Do not store the transparent state in delayed dnets.

We know statically that it is going to be the one provided at the time of
lookup, so we simply fetch it from there.
---
 tactics/hints.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 7d065df19b..db4b23705f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -249,25 +249,25 @@ struct
   module Data = struct type t = stored_data let compare = pri_order_int end
   module Bnet = Btermdn.Make(Data)
 
-  type diff = TransparentState.t option * Pattern.constr_pattern * stored_data
+  type diff = Pattern.constr_pattern * stored_data
   type data = Bnet of Bnet.t | Diff of diff * data ref
   type t = data ref
 
   let empty = ref (Bnet Bnet.empty)
 
-  let add st net p v = ref (Diff ((st, p, v), net))
+  let add _st net p v = ref (Diff ((p, v), net))
 
-  let rec force env net = match !net with
+  let rec force env st net = match !net with
   | Bnet dn -> dn
-  | Diff ((st, p, v), rem) ->
-    let dn = force env rem in
+  | Diff ((p, v), rem) ->
+    let dn = force env st rem in
     let p = Bnet.pattern env st p in
     let dn = Bnet.add dn p v in
     let () = net := (Bnet dn) in
     dn
 
   let lookup env sigma st net p =
-    let dn = force env net in
+    let dn = force env st net in
     Bnet.lookup env sigma st dn p
 end
 
-- 
cgit v1.2.3