aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-11-12 16:40:39 +0000
committerGravatar gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-11-12 16:40:39 +0000
commitf987a343850df4602b3d8020395834d22eb1aea3 (patch)
treec9c23771714f39690e9dc42ce0c58653291d3202 /theories
parent41095b1f02abac5051ab61a91080550bebbb3a7e (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.v2
-rwxr-xr-xtheories/Init/Peano.v1
-rw-r--r--theories/NArith/BinNat.v1
-rw-r--r--theories/NArith/BinPos.v1
-rw-r--r--theories/Reals/Binomial.v2
-rw-r--r--theories/Reals/R_sqrt.v2
-rw-r--r--theories/Reals/Raxioms.v4
-rw-r--r--theories/Reals/Rfunctions.v8
-rw-r--r--theories/Reals/RiemannInt.v2
-rw-r--r--theories/Reals/RiemannInt_SF.v6
-rw-r--r--theories/Reals/Rpower.v6
-rw-r--r--theories/Reals/Rprod.v2
-rw-r--r--theories/Reals/Rseries.v2
-rw-r--r--theories/Reals/Rsqrt_def.v2
-rw-r--r--theories/Reals/Rtrigo_def.v6
-rw-r--r--theories/ZArith/BinInt.v4
-rw-r--r--theories/ZArith/Zbool.v2
-rw-r--r--theories/ZArith/Zdiv.v2
-rw-r--r--theories/ZArith/Zlogarithm.v1
-rw-r--r--theories/ZArith/Zmin.v2
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