From cf755caa0e7e99959da289e798771f4822160613 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 18 Dec 2001 13:56:07 +0000
Subject: ote les redondances des entetes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2309 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/table.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index a45490f201..2eca006c7b 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -173,7 +173,9 @@ let sorted_ml_extractions () = let (_,_,l) = !extractions in l
 
 let add_ml_extraction r s = 
   let (map,set,list) = !extractions in
-  let list' = if (is_constant r) then (r,s)::list else list in 
+  let list' = if (is_constant r) then 
+    (r,s)::(List.remove_assoc r list) 
+  else list in 
   extractions := (Refmap.add r s map, Refset.add r set, list')
 
 let is_ml_extraction r = 
-- 
cgit v1.2.3