bug discharge (work_alist contenanti plein de fois les memes choses)

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

1 files changed, 2 insertions, 4 deletions

diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 09b10538d..859f00a00 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -173,10 +173,8 @@ let process_constant osecsp nsecsp oldenv (ids_to_discard,modlist) cb =
     expmod_constant_value cb.const_opaque oldenv modlist cb.const_body in
   let typ = expmod_type oldenv modlist cb.const_type in
   let hyps = map_sign_typ (expmod_type oldenv modlist) cb.const_hyps in
-  let (body',typ',modl) = 
-    abstract_constant ids_to_discard hyps (body,typ)
-  in
-  let mods = (Const osecsp, DO_ABSTRACT(Const nsecsp,modl)) :: modlist in
+  let (body',typ',modl) = abstract_constant ids_to_discard hyps (body,typ) in
+  let mods = [ (Const osecsp, DO_ABSTRACT(Const nsecsp,modl)) ] in
   (body', typ'.body, mods)