diff options
Diffstat (limited to 'theories/Numbers/Natural')
| -rw-r--r-- | theories/Numbers/Natural/Binary/NBinary.v | 1 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 1 | ||||
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 2 |
3 files changed, 0 insertions, 4 deletions
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index 97e7b36784..34b44d3c60 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -160,7 +160,6 @@ Proof. destruct b; discriminate. Qed. (** Log2 *) -Program Instance log2_wd : Proper (eq==>eq) Nlog2. Definition log2_spec := Nlog2_spec. Definition log2_nonpos := Nlog2_nonpos. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 3255fda683..6502cfa555 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -444,7 +444,6 @@ Definition pow_succ_r := pow_succ_r. Lemma pow_neg_r : forall a b, b<0 -> a^b = 0. inversion 1. Qed. Definition pow := pow. -Program Instance log2_wd : Proper (eq==>eq) log2. Definition log2_spec := log2_spec. Definition log2_nonpos := log2_nonpos. Definition log2 := log2. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 64dcd1967e..3620045d1e 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -245,8 +245,6 @@ Qed. (** Log2 *) -Program Instance log2_wd : Proper (eq==>eq) log2. - Lemma log2_spec : forall n, 0<n -> 2^(log2 n) <= n /\ n < 2^(succ (log2 n)). Proof. |