From 61180c23e5cdb72843c0c180faeab6f43867bdc8 Mon Sep 17 00:00:00 2001
From: BESSON Frederic
Date: Mon, 22 Mar 2021 16:47:11 +0100
Subject: Move destRef outside ConstrMap.add

---
 plugins/micromega/zify.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index b9480e5f94..800dc6cee2 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -78,9 +78,8 @@ module ConstrMap = struct
 
   type 'a t = 'a list Map.t
 
-  let add evd h e m =
-    let r = fst (EConstr.destRef evd h) in
-    Map.update r (function None -> Some [e] | Some l -> Some (e :: l)) m
+  let add gr e m =
+    Map.update gr (function None -> Some [e] | Some l -> Some (e :: l)) m
 
   let empty = Map.empty
 
@@ -603,8 +602,11 @@ module MakeTable (E : Elt) = struct
   let register_hint evd t elt =
     match EConstr.kind evd t with
     | App (c, _) ->
-      E.table := ConstrMap.add evd c (Application t, E.cast elt) !E.table
-    | _ -> E.table := ConstrMap.add evd t (OtherTerm t, E.cast elt) !E.table
+      let gr = fst (EConstr.destRef evd c) in
+      E.table := ConstrMap.add gr (Application t, E.cast elt) !E.table
+    | _ ->
+      let gr = fst (EConstr.destRef evd t) in
+      E.table := ConstrMap.add gr (OtherTerm t, E.cast elt) !E.table
 
   let register_constr env evd c =
     let c = EConstr.of_constr c in
-- 
cgit v1.2.3