diff options
| -rw-r--r-- | pretyping/tacred.ml | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 653a08fdc0..cfd2d919c6 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -24,12 +24,20 @@ type constant_evaluation = (* We use a cache registered as a global table *) -let eval_table = ref Spmap.empty -type frozen = (int * constant_evaluation) Spmap.t +module CstOrdered = + struct + type t = constant + let compare = Pervasives.compare + end +module Cstmap = Map.Make(CstOrdered) + +let eval_table = ref Cstmap.empty + +type frozen = (int * constant_evaluation) Cstmap.t let init () = - eval_table := Spmap.empty + eval_table := Cstmap.empty let freeze () = !eval_table @@ -133,10 +141,10 @@ and descend_consteval cst = let constant_eval (sp,_ as cst) = try - Spmap.find sp !eval_table + Cstmap.find cst !eval_table with Not_found -> begin let v = descend_consteval cst in - eval_table := Spmap.add sp v !eval_table; + eval_table := Cstmap.add cst v !eval_table; v end |