diff options
| author | bertot | 2006-10-16 07:38:44 +0000 |
|---|---|---|
| committer | bertot | 2006-10-16 07:38:44 +0000 |
| commit | 6a66657ecde0b8c16c5ced22ce0f37b86e9c72ee (patch) | |
| tree | c3f8c9236ad2ff3d0cb9fa2afff997e236cc3a27 | |
| parent | 0eaf8212746e473e548c8b28d278d318fdc0d842 (diff) | |
changes the use of lists and notations, to avoid that the notations
from BinList hide the 'List' type as soon as one requires a ring tactic
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9242 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/setoid_ring/BinList.v | 6 | ||||
| -rw-r--r-- | contrib/setoid_ring/Field_theory.v | 2 | ||||
| -rw-r--r-- | contrib/setoid_ring/Ring_theory.v | 1 |
3 files changed, 2 insertions, 7 deletions
diff --git a/contrib/setoid_ring/BinList.v b/contrib/setoid_ring/BinList.v index 28fc1afbad..c3f5bdc9ad 100644 --- a/contrib/setoid_ring/BinList.v +++ b/contrib/setoid_ring/BinList.v @@ -8,7 +8,7 @@ Set Implicit Arguments. Require Import BinPos. -Require Import List. +Require Export List. Open Scope positive_scope. Section LIST. @@ -98,10 +98,6 @@ Section LIST. Qed. End LIST. -Notation list := List.list. -Notation tail := List.tail. -Notation cons := List.cons. -Notation nil := List.nil. Ltac list_fold_right fcons fnil l := match l with diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v index 28f35c1a16..3c43f7baca 100644 --- a/contrib/setoid_ring/Field_theory.v +++ b/contrib/setoid_ring/Field_theory.v @@ -1192,7 +1192,7 @@ Let Subst := PNSubstL cO cI cadd cmul ceqb. (* simplification + rewriting *) Theorem Field_subst_correct : forall l ul fe m n, - PCond l (Fapp Fcons00 (condition (Fnorm fe)) BinList.nil) -> + PCond l (Fapp Fcons00 (condition (Fnorm fe)) nil) -> Mp (Mpc ul) l -> Peq ceqb (Subst (Nnorm (num (Fnorm fe))) (Mpc ul) m n) (Pc cO) = true -> FEeval l fe == 0. diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v index a7dacaa75d..552e0dec73 100644 --- a/contrib/setoid_ring/Ring_theory.v +++ b/contrib/setoid_ring/Ring_theory.v @@ -19,7 +19,6 @@ 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 50, left associativity). Reserved Notation "x ** y" (at level 40, left associativity). Reserved Notation "-- x" (at level 35, right associativity). |