- gros commit sur ring et field: passage des arguments simplifie

- tacinterp.ml: les arguments tactiques de Tactic Notation n'etaient
  pas evalues, laissant des variables libres (symptome: exc Not_found)
- reals: Open Local --> Local Open
- ListTactics: syntaxe des listes



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

3 files changed, 19 insertions, 19 deletions

diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
index 233b40b881..017a2fe2a0 100644
--- a/theories/Lists/ListTactics.v
+++ b/theories/Lists/ListTactics.v
@@ -13,13 +13,13 @@ Require Import List.
 
 Ltac list_fold_right fcons fnil l :=
   match l with
-  | (cons ?x ?tl) => fcons x ltac:(list_fold_right fcons fnil tl)
+  | ?x :: ?tl => fcons x ltac:(list_fold_right fcons fnil tl)
   | nil => fnil
   end.
 
 Ltac lazy_list_fold_right fcons fnil l :=
   match l with
-  | (cons ?x ?tl) => 
+  | ?x :: ?tl => 
        let cont := lazy_list_fold_right fcons fnil in
        fcons x cont tl
   | nil => fnil 
@@ -27,19 +27,19 @@ Ltac lazy_list_fold_right fcons fnil l :=
 
 Ltac list_fold_left fcons fnil l :=
   match l with
-  | (cons ?x ?tl) => list_fold_left fcons ltac:(fcons x fnil) tl
+  | ?x :: ?tl => list_fold_left fcons ltac:(fcons x fnil) tl
   | nil => fnil
   end.
 
 Ltac list_iter f l :=
   match l with
-  | (cons ?x ?tl) => f x; list_iter f tl
+  | ?x :: ?tl => f x; list_iter f tl
   | nil => idtac
   end.
 
 Ltac list_iter_gen seq f l :=
   match l with
-  | (cons ?x ?tl) =>
+  | ?x :: ?tl =>
       let t1 _ := f x in
       let t2 _ := list_iter_gen seq f tl in
       seq t1 t2
@@ -48,30 +48,30 @@ Ltac list_iter_gen seq f l :=
 
 Ltac AddFvTail a l :=
  match l with
- | nil          => constr:(cons a l)
- | (cons a _)   => l
- | (cons ?x ?l) => let l' := AddFvTail a l in constr:(cons x l')
+ | nil      => constr:(a::nil)
+ | a :: _   => l
+ | ?x :: ?l => let l' := AddFvTail a l in constr:(x::l')
  end.
 
 Ltac Find_at a l :=
  let rec find n l :=
    match l with
-   | nil => fail 100 "anomaly: Find_at"
-   | (cons a _) => eval compute in n
-   | (cons _ ?l) => find (Psucc n) l
+   | nil     => fail 100 "anomaly: Find_at"
+   | a :: _  => eval compute in n
+   | _ :: ?l => find (Psucc n) l
    end
  in find 1%positive l.
 
 Ltac check_is_list t :=
   match t with
-  | cons _ ?l => check_is_list l
-  | nil => idtac
-  | _ => fail 100 "anomaly: failed to build a canonical list"
+  | _ :: ?l => check_is_list l
+  | nil     => idtac
+  | _       => fail 100 "anomaly: failed to build a canonical list"
   end.
 
 Ltac check_fv l :=
   check_is_list l;
   match type of l with 
   | list _ => idtac
-  | _ => fail 100 "anomaly: built an ill-typed list"
+  | _      => fail 100 "anomaly: built an ill-typed list"
   end.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 8823e5d5be..55e3896a80 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -19,8 +19,8 @@ Require Export ZArithRing.
 Require Import Omega.
 Require Export RealField.
 
-Open Local Scope Z_scope.
-Open Local Scope R_scope.
+Local Open Scope Z_scope.
+Local Open Scope R_scope.
 
 Implicit Type r : R.
 
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 2f69fb7616..c9f83d639a 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -19,8 +19,8 @@ Require Export Cos_plus.
 Require Import ZArith_base.
 Require Import Zcomplements.
 Require Import Classical_Prop.
-Open Local Scope nat_scope.
-Open Local Scope R_scope.
+Local Open Scope nat_scope.
+Local Open Scope R_scope.
 
 (** sin_PI2 is the only remaining axiom **)
 Axiom sin_PI2 : sin (PI / 2) = 1.