Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la

syntaxe interne de ring_lookup et field_lookup qui n'était pas assez
robuste pour supporter une syntaxe [ ... ] dans constr.  
Déplacement de now_show de List.v vers Tactics.v, déplacement de "[ _ ]"
au niveau 0.



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

4 files changed, 28 insertions, 32 deletions

diff --git a/contrib/setoid_ring/Field_tac.v b/contrib/setoid_ring/Field_tac.v
index fc89022fd..cccee6045 100644
--- a/contrib/setoid_ring/Field_tac.v
+++ b/contrib/setoid_ring/Field_tac.v
@@ -143,12 +143,12 @@ Ltac Field_simplify := Field_simplify_gen ltac:(fun H => rewrite H).
 
 Tactic Notation (at level 0) "field_simplify" constr_list(rl) :=
   let G := Get_goal in
-  field_lookup Field_simplify [] rl [G].
+  field_lookup Field_simplify [] rl G.
 
 Tactic Notation (at level 0) 
   "field_simplify" "[" constr_list(lH) "]" constr_list(rl) :=
   let G := Get_goal in
-  field_lookup Field_simplify [lH] rl [G].
+  field_lookup Field_simplify [lH] rl G.
 
 Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):=   
   let G := Get_goal in
@@ -156,7 +156,7 @@ Tactic Notation "field_simplify" constr_list(rl) "in" hyp(H):=
   let g := fresh "goal" in
   set (g:= G);
   generalize H;clear H;
-  field_lookup Field_simplify [] rl [t];
+  field_lookup Field_simplify [] rl t;
   intro H;
   unfold g;clear g.
 
@@ -167,7 +167,7 @@ Tactic Notation "field_simplify"
   let g := fresh "goal" in
   set (g:= G);
   generalize H;clear H;
-  field_lookup Field_simplify [lH] rl [t];
+  field_lookup Field_simplify [lH] rl t;
   intro H;
   unfold g;clear g.
 
@@ -178,12 +178,12 @@ Ltac Field_simplify_in hyp:=
 Tactic Notation (at level 0) 
   "field_simplify" constr_list(rl) "in" hyp(h) :=
   let t := type of h in
-  field_lookup (Field_simplify_in h) [] rl [t].
+  field_lookup (Field_simplify_in h) [] rl t.
 
 Tactic Notation (at level 0) 
   "field_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h) :=
   let t := type of h in
-  field_lookup (Field_simplify_in h) [lH] rl [t].
+  field_lookup (Field_simplify_in h) [lH] rl t.
 *)
 
 (** Generic tactic for solving equations *)
@@ -242,11 +242,11 @@ Ltac FIELD :=
  
 Tactic Notation (at level 0) "field" :=
   let G := Get_goal in
-  field_lookup FIELD [] [G].
+  field_lookup FIELD [] G.
 
 Tactic Notation (at level 0) "field" "[" constr_list(lH) "]" :=
   let G := Get_goal in
-  field_lookup FIELD [lH] [G].
+  field_lookup FIELD [lH] G.
 
 (* transforms a field equation to an equivalent (simplified) ring equation,
    and leaves non-zero conditions to be proved (field_simplify_eq) *)
@@ -260,11 +260,11 @@ Ltac FIELD_SIMPL  :=
 
 Tactic Notation (at level 0) "field_simplify_eq" :=  
   let G := Get_goal in
-  field_lookup FIELD_SIMPL [] [G].
+  field_lookup FIELD_SIMPL [] G.
 
 Tactic Notation (at level 0) "field_simplify_eq" "[" constr_list(lH) "]" :=  
   let G := Get_goal in
-  field_lookup FIELD_SIMPL [lH] [G].
+  field_lookup FIELD_SIMPL [lH] G.
 
 (* Same as FIELD_SIMPL but in hypothesis *)
 
@@ -323,7 +323,7 @@ Ltac FIELD_SIMPL_EQ :=
 Tactic Notation (at level 0) "field_simplify_eq" "in" hyp(H) :=
   let t := type of H in
   generalize H;
-  field_lookup FIELD_SIMPL_EQ [] [t];
+  field_lookup FIELD_SIMPL_EQ [] t;
   [ try exact I
   | clear H;intro H].
 
@@ -332,7 +332,7 @@ Tactic Notation (at level 0)
   "field_simplify_eq" "[" constr_list(lH) "]"  "in" hyp(H) :=  
   let t := type of H in
   generalize H;
-  field_lookup FIELD_SIMPL_EQ [lH] [t];
+  field_lookup FIELD_SIMPL_EQ [lH] t;
   [ try exact I
   |clear H;intro H].
  
diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v
index d5fc5f348..46d106d37 100644
--- a/contrib/setoid_ring/Ring_tac.v
+++ b/contrib/setoid_ring/Ring_tac.v
@@ -250,11 +250,11 @@ Ltac Get_goal := match goal with [|- ?G] => G end.
 
 Tactic Notation (at level 0) "ring" :=
   let G := Get_goal in
-  ring_lookup Ring_gen [] [G].
+  ring_lookup Ring_gen [] G.
 
 Tactic Notation (at level 0) "ring" "[" constr_list(lH) "]" :=
   let G := Get_goal in
-  ring_lookup Ring_gen [lH] [G].
+  ring_lookup Ring_gen [lH] G.
 
 (* Simplification *)
 
@@ -281,12 +281,12 @@ Ltac Ring_simplify := Ring_simplify_gen ltac:(fun H => rewrite H).
 
 Tactic Notation (at level 0) "ring_simplify" constr_list(rl) := 
   let G := Get_goal in
-  ring_lookup Ring_simplify [] rl [G].
+  ring_lookup Ring_simplify [] rl G.
 
 Tactic Notation (at level 0) 
   "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) :=
   let G := Get_goal in
-  ring_lookup Ring_simplify [lH] rl [G].
+  ring_lookup Ring_simplify [lH] rl G.
 
 (* MON DIEU QUE C'EST MOCHE !!!!!!!!!!!!! *)
 
@@ -296,7 +296,7 @@ Tactic Notation "ring_simplify" constr_list(rl) "in" hyp(H):=
   let g := fresh "goal" in
   set (g:= G);
   generalize H;clear H;
-  ring_lookup Ring_simplify [] rl [t];
+  ring_lookup Ring_simplify [] rl t;
   intro H;
   unfold g;clear g.
 
@@ -307,13 +307,13 @@ Tactic Notation
   let g := fresh "goal" in
   set (g:= G);
   generalize H;clear H;
-  ring_lookup Ring_simplify [lH] rl [t];
+  ring_lookup Ring_simplify [lH] rl t;
   intro H;
   unfold g;clear g.
 
 
 
-(*     LE RESTE MARCHE PAS DOMAGE  .....  *)
+(*     LE RESTE MARCHE PAS DOMMAGE  .....  *)
 
 
 
@@ -343,11 +343,11 @@ Ltac Ring_simplify_in hyp:= Ring_simplify_gen ltac:(fun H => rewrite H in hyp).
 
 Tactic Notation (at level 0) 
   "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) := 
-  match goal with [|- ?G] => ring_lookup Ring_simplify [lH] rl [G] end.
+  match goal with [|- ?G] => ring_lookup Ring_simplify [lH] rl G end.
 
 Tactic Notation (at level 0) 
   "ring_simplify" constr_list(rl) := 
-  match goal with [|- ?G] => ring_lookup Ring_simplify [] rl [G] end.
+  match goal with [|- ?G] => ring_lookup Ring_simplify [] rl G end.
 
 Tactic Notation (at level 0) 
   "ring_simplify" "[" constr_list(lH) "]" constr_list(rl) "in" hyp(h):= 
@@ -357,7 +357,7 @@ Tactic Notation (at level 0)
      pre(); 
      Ring_norm_gen ltac:(fun EQ => rewrite EQ in h) cst_tac pow_tac lemma2 req ring_subst_niter lH rl; 
      post()) 
-  [lH] rl [t]. 
+  [lH] rl t. 
 (*  ring_lookup ltac:(Ring_simplify_in h) [lH] rl [t]. NE MARCHE PAS ??? *)
 
 Ltac Ring_simpl_in hyp := Ring_norm_gen ltac:(fun H => rewrite H in hyp).
@@ -370,7 +370,7 @@ Tactic Notation (at level 0)
      pre(); 
      Ring_simpl_in h cst_tac pow_tac lemma2 req ring_subst_niter lH rl; 
      post())
- [] rl [t].
+ [] rl t.
 
 Ltac rw_in H Heq := rewrite Heq in H.
 
@@ -381,7 +381,7 @@ Ltac simpl_in H :=
      pre(); 
      Ring_norm_gen ltac:(fun Heq => rewrite Heq in H) cst_tac pow_tac lemma2 req ring_subst_niter lH rl; 
      post()) 
-   [] [t].
+   [] t.
 
 
 *)
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v
index 4c542ffdd..b7876130a 100644
--- a/contrib/setoid_ring/Ring_theory.v
+++ b/contrib/setoid_ring/Ring_theory.v
@@ -19,8 +19,6 @@ Reserved Notation "x -! y" (at level 50, left associativity).
 Reserved Notation "x *! y" (at level 40, left associativity).
 Reserved Notation "-! x" (at level 35, right associativity).
 
-Reserved Notation "[ x ]" (at level 1, no associativity).
-
 Reserved Notation "x ?== y" (at level 70, no associativity).
 Reserved Notation "x -- y" (at level 50, left associativity).
 Reserved Notation "x ** y" (at level 40, left associativity).
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index c80b37d91..c3caa403e 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -828,9 +828,8 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl =
           lemma1;lemma2;pretac;posttac;lH;rl])) gl
 
 TACTIC EXTEND ring_lookup
-| [ "ring_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(lr)
-      "[" constr(t) "]" ] ->
-    [ring_lookup (fst f) lH lr t]
+| [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] ->
+    [ let (t,lr) = list_sep_last lrt in ring_lookup (fst f) lH lr t]
 END
 
 
@@ -1163,7 +1162,6 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl =
          field_simpl_eq_in_ok;cond_ok;pretac;posttac;lH;rl])) gl
 
 TACTIC EXTEND field_lookup
-| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(l) 
-     "[" constr(t) "]" ] -> 
-      [ field_lookup (fst f) lH l t ]
+| [ "field_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> 
+      [ let (t,l) = list_sep_last lt in field_lookup (fst f) lH l t ]
 END