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

12 files changed, 56 insertions, 49 deletions

diff --git a/CHANGES b/CHANGES
index bf11db468..2fd30d416 100644
--- a/CHANGES
+++ b/CHANGES
@@ -63,6 +63,7 @@ Libraries (DOC TO CHECK)
   elements, nothing more). 
 - In ListSet, a few definitions are now in Type (may induce a few
   incompatibilities).
+- Notation [t;...;u] for lists made available in list_scope.
 - Changes in FSets/FMaps:
   - Improvements: in particular FMap now provides an induction principle 
     on maps, and some properties about FSets and fold needs less hypotheses.
@@ -99,7 +100,8 @@ Notations, coercions and implicit arguments
   (DOC TODO?)
 - New options Global and Local to "Implicit Arguments" for section
   surviving or non export outside module.
-- Level "constr" moved from 9 to 8. (DOC TODO?)
+- Level "constr" moved from 9 to 8 and notation "[ _ ]" now at level 0
+  (easy to fix in case of incompatibilites). (DOC TODO?)
 - Structure/Record now printed as Record (unless option Printing All is set).
 - Support for parametric notations defining constants.
 - Insertion of coercions below product types refrains to unfold
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index 4f2426337..bb3cfc5a8 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -897,6 +897,6 @@ End rings.
 Infix "+" := Pplus : ring_scope.
 Infix "*" := Pmult : ring_scope.
 Notation "- x" := (Popp x) : ring_scope.
-Notation "[ x ]" := (Pvar x) (at level 1) : ring_scope.
+Notation "[ x ]" := (Pvar x) : ring_scope.
 
 Delimit Scope ring_scope with ring.
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index 46512aab0..31ca8f804 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -879,7 +879,7 @@ Infix "+" := Tplus : romega_scope.
 Infix "*" := Tmult : romega_scope.
 Infix "-" := Tminus : romega_scope.
 Notation "- x" := (Topp x) : romega_scope.
-Notation "[ x ]" := (Tvar x) (at level 1) : romega_scope.
+Notation "[ x ]" := (Tvar x) : romega_scope.
 
 (* \subsubsection{Definition of reified goals} *)
 
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
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index c541b5a7e..f7a538720 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -152,6 +152,7 @@ GEXTEND Gram
   tactic_atom:
     [ [ id = METAIDENT -> MetaIdArg (loc,true,id)
       | n = integer -> Integer n
+      | r = reference -> Reference r
       | "()" -> TacVoid ] ]
   ;
   match_key:
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 7803cd076..d59a46d12 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -244,6 +244,9 @@ GEXTEND Gram
           ExplicitBindings bl
       | bl = LIST1 constr -> ImplicitBindings bl ] ]
   ;
+  opt_bindings:
+    [ [ bl = bindings -> bl | -> NoBindings ] ]
+  ;
   constr_with_bindings:
     [ [ c = constr; l = with_bindings -> (c, l) ] ]
   ;
@@ -527,10 +530,8 @@ GEXTEND Gram
       | IDENT "eright"; bl = with_bindings -> TacRight (true,bl)
       | IDENT "split";  bl = with_bindings -> TacSplit (false,false,bl)
       | IDENT "esplit"; bl = with_bindings -> TacSplit (true,false,bl)
-      | "exists";       bl = bindings -> TacSplit (false,true,bl)
-      | "eexists";      bl = bindings -> TacSplit (true,true,bl)
-      | "exists"  (* meaningless? *)  -> TacSplit (false,true,NoBindings)
-      | "eexists"                     -> TacSplit (true,true,NoBindings)
+      | "exists";        bl = opt_bindings -> TacSplit (false,true,bl)
+      | IDENT "eexists"; bl = opt_bindings -> TacSplit (true,true,bl)
       | IDENT "constructor"; n = num_or_meta; l = with_bindings ->
 	  TacConstructor (false,n,l)
       | IDENT "econstructor"; n = num_or_meta; l = with_bindings ->
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 9a0406d59..0aee1d4ca 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -71,6 +71,8 @@ Reserved Notation "{ x : A  |  P  &  Q }" (at level 0, x at level 99).
 Reserved Notation "{ x : A  &  P }" (at level 0, x at level 99).
 Reserved Notation "{ x : A  &  P  &  Q }" (at level 0, x at level 99).
 
+Reserved Notation "[ x ]" (at level 0).
+
 Delimit Scope type_scope with type.
 Delimit Scope core_scope with core.
 
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index d822a45c5..602b11900 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -152,3 +152,6 @@ match goal with
 | _ => solve [trivial | reflexivity | symmetry; trivial | discriminate | split]
 | _ => fail 1 "Cannot solve this goal"
 end.
+
+(** A tactic to document or check what is proved at some point of a script *)
+Ltac now_show c := change c.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 51d3f192d..2cce009a2 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1,12 +1,12 @@
-  (************************************************************************)
-  (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-  (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-  (*   \VV/  **************************************************************)
-  (*    //   *      This file is distributed under the terms of the       *)
-  (*         *       GNU Lesser General Public License Version 2.1        *)
-  (************************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
-  (*i $Id$ i*)
+(*i $Id$ i*)
 
 Require Import Le Gt Minus Min Bool.
 
@@ -81,9 +81,11 @@ End Lists.
 Implicit Arguments nil [A].
 Infix "::" := cons (at level 60, right associativity) : list_scope.
 Infix "++" := app (right associativity, at level 60) : list_scope.
- 
-Ltac now_show c := change c in |- *.
 
+Notation "[ ]" := nil : list_scope.
+Notation "[ x ]" := (cons x nil) : list_scope.
+Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) .. )) : list_scope.
+ 
 Open Scope list_scope.
 
 Delimit Scope list_scope with list.