- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)

- Changement au passage de la convention "at -n1 ... -n2" en 
  "at - n1 ... n2" qui me paraît plus clair à partir du moment où on peut
  pas mélanger des positifs et des négatifs.
- Au passage:
  - simplification de gclause avec fusion de onconcl et concl_occs,
  - généralisation de l'utilisation de la désignation des occurrences par la
    négative aux cas de setoid_rewrite, clrewrite et rewrite at,
  - correction d'un bug de "rewrite in at" qui utilisait le at de la
    conclusion dans les hyps.


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

1 files changed, 4 insertions, 2 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index a6ae7240ca..0ef8356892 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -527,7 +527,8 @@ let compute_bl_tact ind lnamesparrec nparrec  =
                      tclTRY ( 
                       tclORELSE reflexivity (Equality.discr_tac None)
                      );
-                     simpl_in_hyp (([],freshz),Tacexpr.InHyp);
+                     simpl_in_hyp
+		       ((Rawterm.all_occurrences_expr,freshz),Tacexpr.InHyp);
 (*
 repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
 *)
@@ -798,7 +799,8 @@ let compute_dec_tact ind lnamesparrec nparrec =
             (tclTHENSEQ [apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs));
                       Auto.default_auto
             ]);
-         Pfedit.by (Equality.general_rewrite_bindings_in true []
+         Pfedit.by (Equality.general_rewrite_bindings_in true
+	                      all_occurrences
                               (List.hd !avoid) 
                               ((mkVar (List.hd (List.tl !avoid))),
                                 Rawterm.NoBindings