cache pour les constantes

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

1 files changed, 13 insertions, 5 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 4aebbe7b91..9dff1a4249 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -263,6 +263,9 @@ let add_constructor_extraction c e =
 
 let lookup_constructor_extraction i = Gmap.find i !constructor_extraction_table
 
+let constant_table = 
+  ref (Gmap.empty : (section_path, extraction_result) Gmap.t)
+
 (*s Extraction of a type. *)
 
 (* When calling [extract_type] we suppose that the type of [c] is an
@@ -553,11 +556,16 @@ and extract_constr env ctx c =
 (*s Extraction of a constant. *)
 		
 and extract_constant sp =
-  (* TODO: Axioms *)
-  let cb = Global.lookup_constant sp in
-  let typ = cb.const_type in
-  let body = match cb.const_body with Some c -> c | None -> assert false in
-  extract_constr_with_type (Global.env()) [] body typ
+  try
+    Gmap.find sp !constant_table
+  with Not_found ->
+    (* TODO: Axioms *)
+    let cb = Global.lookup_constant sp in
+    let typ = cb.const_type in
+    let body = match cb.const_body with Some c -> c | None -> assert false in
+    let e = extract_constr_with_type (Global.env()) [] body typ in
+    constant_table := Gmap.add sp e !constant_table;
+    e
     
 (*s Extraction of an inductive. *)