From ff599471c8b037a5033724e54657cfe15d0bd681 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 5 Apr 2008 21:45:09 +0000 Subject: - 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). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10760 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/vernacentries.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel') 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" ) -- cgit v1.2.3