- Retour en arrière sur la capacité du nouvel apply à utiliser les

  lemmes se terminant par False ou not sur n'importe quelle formule
  (cela crée trop d'incompatibilités dans les "try apply" etc.); de
  toutes façons, "contradict" joue presque ce rôle (à ceci près qu'il
  ne traverse pas les conjonctions) (tactics/tactics.ml).
- Quelques corrections sur RIneq.v
  - le  hint Rlt_not_eq avait été oublié dans la phase de restructuration,
  - davantage de noms canoniques (O -> 0, etc.),
  - nouvelle tentative de ramener "auto" vers Rle (avec Rle_ge) plutôt
    que vers Rge qui est moins souvent associé à des hints.
- Utilisation du formateur deep_ft pour afficher les scripts de preuve afin
  d'éviter le besoin d'un "Set Printing Depth" (vernacentries.ml).
- Suppression de certaines utilisations de l'Anomaly de meta_fvalue
  qui ne correspondaient pas à des comportements anormaux (reductionops.ml).



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

0 files changed, 0 insertions, 0 deletions