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

3 files changed, 17 insertions, 10 deletions

diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 9a0406d591..0aee1d4ca7 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 d822a45c50..602b119007 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 51d3f192dc..2cce009a27 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.