Tables des eval_constant devient une Cstmap

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@855 85f007b7-540e-0410-9357-904b9bb8a0f7

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