diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-18 13:56:07 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-18 13:56:07 +0000 |
| commit | cf755caa0e7e99959da289e798771f4822160613 (patch) | |
| tree | e42319ea9b11609734d9cde8ce6922b0fc0f8b8e /contrib | |
| parent | 09f8cdaf5476a7519d54658f40ebbda0a88b0578 (diff) | |
ote les redondances des entetes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2309 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/extraction/table.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index a45490f20..2eca006c7 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 = |