correctifs de bug pour romega:

1) dans refl_omega, on donnait a OmegaSolver un generateur de numero
d'equations new_eq_id qui pouvait clasher avec les numeros d'equations 
initiaux créés avec new_omega_id.
=> 
on sépare en deux compteurs, un pour les equations omegas, l'autre 
pour les variables omegas. On en profite pour reinitialiser ces 
compteurs à chaque session romega, histoire que romega devienne 
reproductible. 

2) dans omega.ml, le role de new_eq_id et new_var_id etait interverti 
à un endroit. 
ATTENTION: ceci peut changer le comportement d'omega. Surveiller le 
resultat du prochain bench nocturne. 

3) dans ReflOmegaCore.v, on ne traitait pas le cas d'une implication 
dans une hypothese lors du recalcul final. 




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

0 files changed, 0 insertions, 0 deletions