diff options
Diffstat (limited to 'theories/Arith/Max.v')
| -rw-r--r-- | theories/Arith/Max.v | 58 |
1 files changed, 31 insertions, 27 deletions
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index d1b1b269..77dfa508 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -1,44 +1,48 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Max.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +(** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *) -(** THIS FILE IS DEPRECATED. Use [MinMax] instead. *) - -Require Export MinMax. +Require Import NPeano. Local Open Scope nat_scope. Implicit Types m n p : nat. -Notation max := MinMax.max (only parsing). - -Definition max_0_l := max_0_l. -Definition max_0_r := max_0_r. -Definition succ_max_distr := succ_max_distr. -Definition plus_max_distr_l := plus_max_distr_l. -Definition plus_max_distr_r := plus_max_distr_r. -Definition max_case_strong := max_case_strong. -Definition max_spec := max_spec. -Definition max_dec := max_dec. -Definition max_case := max_case. -Definition max_idempotent := max_id. -Definition max_assoc := max_assoc. -Definition max_comm := max_comm. -Definition max_l := max_l. -Definition max_r := max_r. -Definition le_max_l := le_max_l. -Definition le_max_r := le_max_r. -Definition max_lub_l := max_lub_l. -Definition max_lub_r := max_lub_r. -Definition max_lub := max_lub. +Notation max := Peano.max (only parsing). + +Definition max_0_l := Nat.max_0_l. +Definition max_0_r := Nat.max_0_r. +Definition succ_max_distr := Nat.succ_max_distr. +Definition plus_max_distr_l := Nat.add_max_distr_l. +Definition plus_max_distr_r := Nat.add_max_distr_r. +Definition max_case_strong := Nat.max_case_strong. +Definition max_spec := Nat.max_spec. +Definition max_dec := Nat.max_dec. +Definition max_case := Nat.max_case. +Definition max_idempotent := Nat.max_id. +Definition max_assoc := Nat.max_assoc. +Definition max_comm := Nat.max_comm. +Definition max_l := Nat.max_l. +Definition max_r := Nat.max_r. +Definition le_max_l := Nat.le_max_l. +Definition le_max_r := Nat.le_max_r. +Definition max_lub_l := Nat.max_lub_l. +Definition max_lub_r := Nat.max_lub_r. +Definition max_lub := Nat.max_lub. (* begin hide *) (* Compatibility *) Notation max_case2 := max_case (only parsing). -Notation max_SS := succ_max_distr (only parsing). +Notation max_SS := Nat.succ_max_distr (only parsing). (* end hide *) + +Hint Resolve + Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r : arith v62. + +Hint Resolve + Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r : arith v62. |