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.

1 files 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