- 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

1 files changed, 1 insertions, 1 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f5768888c..23f26038e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -95,7 +95,7 @@ let show_script () =
   let pts = get_pftreestate () in
   let pf = proof_of_pftreestate pts
   and evc = evc_of_pftreestate pts in
-  msgnl (print_treescript true evc pf)
+  msgnl_with Pp_control.deep_ft (print_treescript true evc pf)
 
 let show_thesis () =
      msgnl (anomaly "TODO" )