diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/micromega/zify.ml | 12 |
1 files changed, 7 insertions, 5 deletions
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 |