Remove the "Boxed" syntaxes and the const_entry_boxed field

 According to B. Gregoire, this stuff is obsolete. Fine control
 on when to launch the VM in conversion problems is now provided
 by VMcast. We were already almost never boxing definitions anymore
 in stdlib files.

 "(Un)Boxed Definition foo" will now trigger a parsing error,
 same with Fixpoint. The option "(Un)Set Boxed Definitions"
 aren't there anymore, but tolerated (as no-ops), since unknown
 options raise a warning instead of an error by default.

 Some more cleaning could be done in the vm.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7

13 files changed, 9 insertions, 22 deletions

diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index fd902aa841..1dd5ce16cb 100644
--- a/theories/Arith/Factorial.v
+++ b/theories/Arith/Factorial.v
@@ -13,7 +13,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 216ca35af4..03487b6d67 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -26,7 +26,6 @@
 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 81e2e06e47..686a0692ce 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 Require Import BinPos.
-Unset Boxed Definitions.
 
 (**********************************************************************)
 (** Binary natural numbers *)
diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v
index 97d935e4f7..d2e6c70b92 100644
--- a/theories/Numbers/Cyclic/Int31/Int31.v
+++ b/theories/Numbers/Cyclic/Int31/Int31.v
@@ -13,8 +13,6 @@ Require Import Wf_nat.
 Require Export ZArith.
 Require Export DoubleType.
 
-Unset Boxed Definitions.
-
 (** * 31-bit integers *)
 
 (** This file contains basic definitions of a 31-bit integer
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 0ffce766c0..64e32c560a 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -7,8 +7,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Unset Boxed Definitions.
-
 Declare ML Module "z_syntax_plugin".
 
 (**********************************************************************)
@@ -65,8 +63,6 @@ Fixpoint Psucc (x:positive) : positive :=
 
 (** ** Addition *)
 
-Set Boxed Definitions.
-
 Fixpoint Pplus (x y:positive) : positive :=
   match x, y with
     | p~1, q~1 => (Pplus_carry p q)~0
@@ -93,8 +89,6 @@ with Pplus_carry (x y:positive) : positive :=
     | 1, 1 => 1~1
   end.
 
-Unset Boxed Definitions.
-
 Infix "+" := Pplus : positive_scope.
 
 Definition Piter_op {A}(op:A->A->A) :=
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index cbf6da1970..e858d2148e 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -105,7 +105,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
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 525eff6887..1eee8d8524 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -659,7 +659,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) : nat :=
+Fixpoint sum_nat_f_O (f:nat -> nat) (n:nat) : nat :=
   match n with
     | O => f 0%nat
     | S n' => (sum_nat_f_O f n' + f (S n'))%nat
diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v
index 0687bfbc23..d16e7f2c75 100644
--- a/theories/Reals/RiemannInt_SF.v
+++ b/theories/Reals/RiemannInt_SF.v
@@ -147,7 +147,7 @@ Definition subdivision_val (a b:R) (f:StepFun a b) : Rlist :=
     | existT a b => a
   end.
 
-Boxed Fixpoint Int_SF (l k:Rlist) : R :=
+Fixpoint Int_SF (l k:Rlist) : R :=
   match l with
     | nil => 0
     | cons a l' =>
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index 76d66ca062..12258d6b5c 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -15,7 +15,7 @@ Require Import Binomial.
 Open Local Scope R_scope.
 
 (** TT Ak; 0<=k<=N *)
-Boxed Fixpoint prod_f_R0 (f:nat -> R) (N:nat) : R :=
+Fixpoint prod_f_R0 (f:nat -> R) (N:nat) : R :=
   match N with
     | O => f O
     | S p => prod_f_R0 f p * f (S p)
diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 5f8b5d9da2..479d381d4a 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -25,7 +25,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 2fdf1ffead..8c46f355f0 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -13,7 +13,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/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index a5fdf855a2..ad3781832a 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -15,8 +15,6 @@
 Require Export BinPos Pnat.
 Require Import BinNat Plus Mult.
 
-Unset Boxed Definitions.
-
 Inductive Z : Set :=
   | Z0 : Z
   | Zpos : positive -> Z
@@ -1002,13 +1000,13 @@ Qed.
 (**********************************************************************)
 (** * Minimum and maximum *)
 
-Unboxed Definition Zmax (n m:Z) :=
+Definition Zmax (n m:Z) :=
   match n ?= m with
     | Eq | Gt => n
     | Lt => m
   end.
 
-Unboxed Definition Zmin (n m:Z) :=
+Definition Zmin (n m:Z) :=
   match n ?= m with
     | Eq | Lt => n
     | Gt => m
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index 4f4a6078c0..45fcc17bec 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -13,7 +13,6 @@ Require Import Zcompare.
 Require Import ZArith_dec.
 Require Import Sumbool.
 
-Unset Boxed Definitions.
 Open Local Scope Z_scope.
 
 (** * Boolean operations from decidability of order *)