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

2 files changed, 2 insertions, 5 deletions

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index a5fdf855a..ad3781832 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 4f4a6078c..45fcc17be 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 *)