diff options
Diffstat (limited to 'theories/Arith/Min.v')
| -rw-r--r-- | theories/Arith/Min.v | 52 |
1 files changed, 25 insertions, 27 deletions
diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 0c8b5669..bcfbe0ef 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -1,44 +1,42 @@ (************************************************************************) (* 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: Min.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. Open Local Scope nat_scope. Implicit Types m n p : nat. -Notation min := MinMax.min (only parsing). +Notation min := Peano.min (only parsing). -Definition min_0_l := min_0_l. -Definition min_0_r := min_0_r. -Definition succ_min_distr := succ_min_distr. -Definition plus_min_distr_l := plus_min_distr_l. -Definition plus_min_distr_r := plus_min_distr_r. -Definition min_case_strong := min_case_strong. -Definition min_spec := min_spec. -Definition min_dec := min_dec. -Definition min_case := min_case. -Definition min_idempotent := min_id. -Definition min_assoc := min_assoc. -Definition min_comm := min_comm. -Definition min_l := min_l. -Definition min_r := min_r. -Definition le_min_l := le_min_l. -Definition le_min_r := le_min_r. -Definition min_glb_l := min_glb_l. -Definition min_glb_r := min_glb_r. -Definition min_glb := min_glb. +Definition min_0_l := Nat.min_0_l. +Definition min_0_r := Nat.min_0_r. +Definition succ_min_distr := Nat.succ_min_distr. +Definition plus_min_distr_l := Nat.add_min_distr_l. +Definition plus_min_distr_r := Nat.add_min_distr_r. +Definition min_case_strong := Nat.min_case_strong. +Definition min_spec := Nat.min_spec. +Definition min_dec := Nat.min_dec. +Definition min_case := Nat.min_case. +Definition min_idempotent := Nat.min_id. +Definition min_assoc := Nat.min_assoc. +Definition min_comm := Nat.min_comm. +Definition min_l := Nat.min_l. +Definition min_r := Nat.min_r. +Definition le_min_l := Nat.le_min_l. +Definition le_min_r := Nat.le_min_r. +Definition min_glb_l := Nat.min_glb_l. +Definition min_glb_r := Nat.min_glb_r. +Definition min_glb := Nat.min_glb. (* begin hide *) (* Compatibility *) Notation min_case2 := min_case (only parsing). -Notation min_SS := succ_min_distr (only parsing). -(* end hide *)
\ No newline at end of file +Notation min_SS := Nat.succ_min_distr (only parsing). +(* end hide *) |