diff options
author | 2004-11-12 16:40:39 +0000 | |
---|---|---|
committer | 2004-11-12 16:40:39 +0000 | |
commit | f987a343850df4602b3d8020395834d22eb1aea3 (patch) | |
tree | c9c23771714f39690e9dc42ce0c58653291d3202 /theories | |
parent | 41095b1f02abac5051ab61a91080550bebbb3a7e (diff) |
Changement dans les boxed values .
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Arith/Factorial.v | 2 | ||||
-rwxr-xr-x | theories/Init/Peano.v | 1 | ||||
-rw-r--r-- | theories/NArith/BinNat.v | 1 | ||||
-rw-r--r-- | theories/NArith/BinPos.v | 1 | ||||
-rw-r--r-- | theories/Reals/Binomial.v | 2 | ||||
-rw-r--r-- | theories/Reals/R_sqrt.v | 2 | ||||
-rw-r--r-- | theories/Reals/Raxioms.v | 4 | ||||
-rw-r--r-- | theories/Reals/Rfunctions.v | 8 | ||||
-rw-r--r-- | theories/Reals/RiemannInt.v | 2 | ||||
-rw-r--r-- | theories/Reals/RiemannInt_SF.v | 6 | ||||
-rw-r--r-- | theories/Reals/Rpower.v | 6 | ||||
-rw-r--r-- | theories/Reals/Rprod.v | 2 | ||||
-rw-r--r-- | theories/Reals/Rseries.v | 2 | ||||
-rw-r--r-- | theories/Reals/Rsqrt_def.v | 2 | ||||
-rw-r--r-- | theories/Reals/Rtrigo_def.v | 6 | ||||
-rw-r--r-- | theories/ZArith/BinInt.v | 4 | ||||
-rw-r--r-- | theories/ZArith/Zbool.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zdiv.v | 2 | ||||
-rw-r--r-- | theories/ZArith/Zlogarithm.v | 1 | ||||
-rw-r--r-- | theories/ZArith/Zmin.v | 2 |
20 files changed, 33 insertions, 25 deletions
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 9f7de8503..987d42eea 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -15,7 +15,7 @@ Open Local Scope nat_scope. (** Factorial *) -Boxed Fixpoint fact (n:nat) : nat := +Fixpoint fact (n:nat) : nat := match n with | O => 1 | S n => S n * fact n diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index c575ba583..b4ce93819 100755 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -26,6 +26,7 @@ Require Import Notations. Require Import Datatypes. Require Import Logic. +Unset Boxed Definitions. Open Scope nat_scope. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 0fd846b2f..6676ea3bf 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -9,6 +9,7 @@ (*i $Id$ i*) Require Import BinPos. +Unset Boxed Definitions. (**********************************************************************) (** Binary natural numbers *) diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index 8e709a489..189e1d15e 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -12,6 +12,7 @@ (** Binary positive numbers *) (** Original development by Pierre Crégut, CNET, Lannion, France *) +Unset Boxed Definitions. Inductive positive : Set := | xI : positive -> positive diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v index 85a3102a0..5c25ae966 100644 --- a/theories/Reals/Binomial.v +++ b/theories/Reals/Binomial.v @@ -13,7 +13,7 @@ Require Import Rfunctions. Require Import PartSum. Open Local Scope R_scope. -Boxed Definition C (n p:nat) : R := +Definition C (n p:nat) : R := INR (fact n) / (INR (fact p) * INR (fact (n - p))). Lemma pascal_step1 : forall n i:nat, (i <= n)%nat -> C n i = C n (n - i). diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index 2f2a52d08..47fc4b016 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -13,7 +13,7 @@ Require Import Rfunctions. Require Import Rsqrt_def. Open Local Scope R_scope. (* Here is a continuous extension of Rsqrt on R *) -Boxed Definition sqrt (x:R) : R := +Definition sqrt (x:R) : R := match Rcase_abs x with | left _ => 0 | right a => Rsqrt (mknonnegreal x (Rge_le _ _ a)) diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 1acd611d5..1fdf145e9 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -107,7 +107,7 @@ Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real. (**********************************************************) (**********) -Boxed Fixpoint INR (n:nat) : R := +Fixpoint INR (n:nat) : R := match n with | O => 0 | S O => 1 @@ -121,7 +121,7 @@ Arguments Scope INR [nat_scope]. (**********************************************************) (**********) -Boxed Definition IZR (z:Z) : R := +Definition IZR (z:Z) : R := match z with | Z0 => 0 | Zpos n => INR (nat_of_P n) diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 3e1a9262d..324ebb98f 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -63,7 +63,7 @@ Qed. (* Power *) (*******************************) (*********) -Boxed Fixpoint pow (r:R) (n:nat) {struct n} : R := +Fixpoint pow (r:R) (n:nat) {struct n} : R := match n with | O => 1 | S n => r * pow r n @@ -527,7 +527,7 @@ Qed. Ltac case_eq name := generalize (refl_equal name); pattern name at -1 in |- *; case name. -Boxed Definition powerRZ (x:R) (n:Z) := +Definition powerRZ (x:R) (n:Z) := match n with | Z0 => 1 | Zpos p => x ^ nat_of_P p @@ -670,7 +670,7 @@ Definition decimal_exp (r:R) (z:Z) : R := (r * 10 ^Z z). (** Sum of n first naturals *) (*******************************) (*********) -Boxed Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) {struct n} : nat := +Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) {struct n} : nat := match n with | O => f 0%nat | S n' => (sum_nat_f_O f n' + f (S n'))%nat @@ -690,7 +690,7 @@ Definition sum_nat (s n:nat) : nat := sum_nat_f s n (fun x:nat => x). (** Sum *) (*******************************) (*********) -Boxed Fixpoint sum_f_R0 (f:nat -> R) (N:nat) {struct N} : R := +Fixpoint sum_f_R0 (f:nat -> R) (N:nat) {struct N} : R := match N with | O => f 0%nat | S i => sum_f_R0 f i + f (S i) diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 7f86f3f42..fe0ed965e 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -461,7 +461,7 @@ assert (H5 := IZN _ H4); elim H5; clear H5; intros N H5; elim (Rlt_irrefl _ H7) ] ]. Qed. -Boxed Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) {struct N} : Rlist := +Fixpoint SubEquiN (N:nat) (x y:R) (del:posreal) {struct N} : Rlist := match N with | O => cons y nil | S p => cons x (SubEquiN p (x + del) y del) diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index d35672404..4dcdebdd1 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -142,12 +142,12 @@ Record StepFun (a b:R) : Type := mkStepFun Definition subdivision (a b:R) (f:StepFun a b) : Rlist := projT1 (pre f). -Boxed Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist := +Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist := match projT2 (pre f) with | existT a b => a end. -Boxed Fixpoint Int_SF (l k:Rlist) {struct l} : R := +Fixpoint Int_SF (l k:Rlist) {struct l} : R := match l with | nil => 0 | cons a l' => @@ -159,7 +159,7 @@ Boxed Fixpoint Int_SF (l k:Rlist) {struct l} : R := end. (* Integral of step functions *) -Boxed Definition RiemannInt_SF (a b:R) (f:StepFun a b) : R := +Definition RiemannInt_SF (a b:R) (f:StepFun a b) : R := match Rle_dec a b with | left _ => Int_SF (subdivision_val f) (subdivision f) | right _ => - Int_SF (subdivision_val f) (subdivision f) diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index 30dfa6274..d850d7f89 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -195,13 +195,13 @@ apply Rinv_neq_0_compat; red in |- *; intro; rewrite H3 in H; Qed. (* Definition of log R+* -> R *) -Boxed Definition Rln (y:posreal) : R := +Definition Rln (y:posreal) : R := match ln_exists (pos y) (cond_pos y) with | existT a b => a end. (* Extension on R *) -Boxed Definition ln (x:R) : R := +Definition ln (x:R) : R := match Rlt_dec 0 x with | left a => Rln (mkposreal x a) | right a => 0 @@ -377,7 +377,7 @@ Qed. (* Definition of Rpower *) (******************************************************************) -Boxed Definition Rpower (x y:R) := exp (y * ln x). +Definition Rpower (x y:R) := exp (y * ln x). Infix Local "^R" := Rpower (at level 30, right associativity) : R_scope. diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index b29fb6a98..85f5af5e0 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -17,7 +17,7 @@ Require Import Binomial. Open Local Scope R_scope. (* TT Ak; 1<=k<=N *) -Boxed Fixpoint prod_f_SO (An:nat -> R) (N:nat) {struct N} : R := +Fixpoint prod_f_SO (An:nat -> R) (N:nat) {struct N} : R := match N with | O => 1 | S p => prod_f_SO An p * An (S p) diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 6d3457229..9bab638af 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -28,7 +28,7 @@ Section sequence. Variable Un : nat -> R. (*********) -Boxed Fixpoint Rmax_N (N:nat) : R := +Fixpoint Rmax_N (N:nat) : R := match N with | O => Un 0 | S n => Rmax (Un (S n)) (Rmax_N n) diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index df750b9c6..1be5cacc6 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -15,7 +15,7 @@ Require Import SeqSeries. Require Import Ranalysis1. Open Local Scope R_scope. -Boxed Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R := +Fixpoint Dichotomy_lb (x y:R) (P:R -> bool) (N:nat) {struct N} : R := match N with | O => x | S n => diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 3d848a948..f8204834e 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -35,7 +35,7 @@ unfold Pser, exp_in in |- *. trivial. Defined. -Boxed Definition exp (x:R) : R := projT1 (exist_exp x). +Definition exp (x:R) : R := projT1 (exist_exp x). Lemma pow_i : forall i:nat, (0 < i)%nat -> 0 ^ i = 0. intros; apply pow_ne_zero. @@ -235,7 +235,7 @@ Qed. (* Definition of cosinus *) (*************************) -Boxed Definition cos (x:R) : R := +Definition cos (x:R) : R := match exist_cos (Rsqr x) with | existT a b => a end. @@ -356,7 +356,7 @@ Qed. (***********************) (* Definition of sinus *) -Boxed Definition sin (x:R) : R := +Definition sin (x:R) : R := match exist_sin (Rsqr x) with | existT a b => x * a end. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 10e7def9e..16e2ff325 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -17,6 +17,8 @@ Require Export Pnat. Require Import BinNat. Require Import Plus. Require Import Mult. + +Unset Boxed Definitions. (**********************************************************************) (** Binary integer numbers *) @@ -1035,4 +1037,4 @@ Definition Zabs_N (z:Z) := Definition Z_of_N (x:N) := match x with | N0 => Z0 | Npos p => Zpos p - end.
\ No newline at end of file + end. diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v index bc92eca14..d49bbfc68 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.v @@ -15,6 +15,8 @@ Require Import Zcompare. Require Import ZArith_dec. Require Import Sumbool. +Unset Boxed Definitions. + (** The decidability of equality and order relations over type [Z] give some boolean functions with the adequate specification. *) diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index c4dca7121..025e03d4a 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -36,7 +36,7 @@ Open Local Scope Z_scope. *) -Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} : +Unboxed Fixpoint Zdiv_eucl_POS (a:positive) (b:Z) {struct a} : Z * Z := match a with | xH => if Zge_bool b 2 then (0, 1) else (1, 0) diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index 25b05cdc7..c45355133 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -36,6 +36,7 @@ Fixpoint log_inf (p:positive) : Z := | xO q => Zsucc (log_inf q) (* 2n *) | xI q => Zsucc (log_inf q) (* 2n+1 *) end. + Fixpoint log_sup (p:positive) : Z := match p with | xH => 0 (* 1 *) diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index 62a6aaf14..d7ebad149 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -19,7 +19,7 @@ Open Local Scope Z_scope. (**********************************************************************) (** Minimum on binary integer numbers *) -Definition Zmin (n m:Z) := +Unboxed Definition Zmin (n m:Z) := match n ?= m return Z with | Eq => n | Lt => n |