- 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, 0 insertions, 6 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index fca11a888b..963025c3b2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -716,12 +716,6 @@ let apply_with_ebindings_gen advanced with_evars (c,lbind) gl =
 		      (List.map (fun id ->
 			tclTHEN (try_main_apply (mkVar id)) (thin l)) l))
 		]) gl
-	    | None -> 
-	    match match_with_empty_type (snd (decompose_prod t)) with
-	    | Some _ ->
-	      let sort = elimination_sort_of_goal gl in
-	      let elim = pf_apply make_case_gen gl mind sort in
-	      general_elim with_evars (c,NoBindings) (elim,NoBindings) gl
 	    | None ->
 	      raise exn
 	  else