Bonjour,

  En debugguant Coq avec Judicael, nous avons obtenu le resultat surprenant
suivant : soit toto.ml le programme suivant

------------------------
#open "hashtbl";;

let f x = 
  let t = new 10
  in add t x true;
     find t x
;;

if f 1 then output_string std_out "ok\n" ; flush std_out
;;
-----------------------

toujours dans le meme repertoire, je fais

-----------------------
% camlc toto.ml
% camlmktop -o essai toto.zo
% camllight essai
ok
>       Caml Light version 0.61
 
#trace "hashtbl__add";;
>> hashtbl__add is now traced.
- : unit = ()
##open "toto";;
hashtbl__add <-- <abstract>
hashtbl__add --> <fun>
hashtbl__add* <-- <poly>
hashtbl__add* --> <fun>
hashtbl__add** <-- <poly>
hashtbl__add** --> ()
#
-----------------------

qu'est-ce qui se passe ?!?!

--Jean-Christophe.