diff options
| -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). |