- 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/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 66246faf5f..92f74d1d94 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -826,9 +826,11 @@ let raw_polynom th op lc gl =
 				     c'''i; ci; c'i_eq_c''i |]))))
 	      (tclTHENS
 		 (tclORELSE
-                   (Setoid_replace.general_s_rewrite true [] c'i_eq_c''i
+                   (Setoid_replace.general_s_rewrite true
+		     Termops.all_occurrences c'i_eq_c''i
                      ~new_goals:[])
-                   (Setoid_replace.general_s_rewrite false [] c'i_eq_c''i
+                   (Setoid_replace.general_s_rewrite false 
+		     Termops.all_occurrences c'i_eq_c''i
                      ~new_goals:[]))
                  [tac]))
 	 else