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

14 files changed, 25 insertions, 41 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 9c00af5dff..337b907512 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -714,18 +714,13 @@ let compile env c =
   Format.print_flush();  *)
   init_code,!fun_code, Array.of_list fv
 
-let compile_constant_body env body opaque boxed =
+let compile_constant_body env body opaque =
   if opaque then BCconstant
   else match body with
   | None -> BCconstant
   | Some sb ->
       let body = Declarations.force sb in
-      if boxed then
-	let res = compile env body in
-	let to_patch = to_memory res in
-	BCdefined(true, to_patch)
-      else
-	match kind_of_term body with
+      match kind_of_term body with
 	| Const kn' ->
 	    (* we use the canonical name of the constant*)
 	    let con= constant_of_kn (canonical_con kn') in
@@ -733,7 +728,7 @@ let compile_constant_body env body opaque boxed =
 	| _ ->
 	    let res = compile env body in
 	    let to_patch = to_memory res in
-	    BCdefined (false, to_patch)
+	    BCdefined to_patch
 
 
 (* spiwack: additional function which allow different part of compilation of the
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index bf9c0be263..403c1c7b5b 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -10,8 +10,8 @@ val compile : env -> constr -> bytecodes * bytecodes * fv
                               (** init, fun, fv *)
 
 val compile_constant_body :
-    env -> constr_substituted option -> bool -> bool -> body_code
-                                 (** opaque *) (* boxed *)
+    env -> constr_substituted option -> bool -> body_code
+                                 (** opaque *)
 
 
 (** spiwack: this function contains the information needed to perform
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 1138031c7a..277b343b24 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -331,12 +331,12 @@ let subst_to_patch s (code,pl,fv) =
   code,List.rev_map (subst_patch s) pl,fv
 
 type body_code =
-  | BCdefined of bool * to_patch
+  | BCdefined of to_patch
   | BCallias of constant
   | BCconstant
 
 let subst_body_code s = function
-  | BCdefined (b,tp) -> BCdefined (b,subst_to_patch s tp)
+  | BCdefined tp -> BCdefined (subst_to_patch s tp)
   | BCallias kn -> BCallias (fst (subst_con s kn))
   | BCconstant -> BCconstant
 
@@ -348,11 +348,6 @@ let force = force subst_body_code
 
 let subst_to_patch_subst = subst_substituted
 
-let is_boxed tps =
-  match force tps with
-  | BCdefined(b,_) -> b
-  | _ -> false
-
 let to_memory (init_code, fun_code, fv) =
   init();
   emit init_code;
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index a8ecc82b41..43cebb4748 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -22,7 +22,7 @@ type to_patch = emitcodes * (patch list) * fv
 val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
 
 type body_code =
-  | BCdefined of bool*to_patch
+  | BCdefined of to_patch
   | BCallias of constant
   | BCconstant
 
@@ -33,8 +33,6 @@ val from_val : body_code -> to_patch_substituted
 
 val force : to_patch_substituted -> body_code
 
-val is_boxed : to_patch_substituted -> bool
-
 val subst_to_patch_subst : Mod_subst.substitution -> to_patch_substituted -> to_patch_substituted
 
 val to_memory : bytecodes * bytecodes * fv -> to_patch
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index e4336683d1..d01398841c 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -137,5 +137,4 @@ let cook_constant env r =
 	let j = make_judge (force (Option.get body)) typ in
 	Typeops.make_polymorphic_if_constant_for_ind env j
   in
-  let boxed = Cemitcodes.is_boxed cb.const_body_code in
-  (body, typ, cb.const_constraints, cb.const_opaque, boxed,false)
+  (body, typ, cb.const_constraints, cb.const_opaque, false)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 0f604a4bee..09b42d0b12 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -24,7 +24,7 @@ type recipe = {
 val cook_constant :
   env -> recipe ->
     constr_substituted option * constant_type * constraints * bool * bool
-  * bool
+
 
 (** {6 Utility functions used in module [Discharge]. } *)
 
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 983c1f26df..897cbf13a8 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -125,10 +125,9 @@ let rec slot_for_getglobal env kn =
   with NotEvaluated ->
     let pos =
       match Cemitcodes.force cb.const_body_code with
-      | BCdefined(boxed,(code,pl,fv)) ->
+      | BCdefined(code,pl,fv) ->
 	let v = eval_to_patch env (code,pl,fv) in
-  	if boxed then set_global_boxed kn v
-	else set_global v
+	set_global v
     | BCallias kn' -> slot_for_getglobal env kn'
     | BCconstant -> set_global (val_of_constant kn) in
     rk := Some pos;
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 714da03196..dbf802bb12 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -57,8 +57,7 @@ type mutual_inductive_entry = {
 type definition_entry = {
   const_entry_body   : constr;
   const_entry_type   : types option;
-  const_entry_opaque : bool;
-  const_entry_boxed  : bool}
+  const_entry_opaque : bool }
 
 (* type and the inlining flag *)
 type parameter_entry = types * bool
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 2ba3064550..d45e2bbdb8 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -53,8 +53,7 @@ type mutual_inductive_entry = {
 type definition_entry = {
   const_entry_body   : constr;
   const_entry_type   : types option;
-  const_entry_opaque : bool;
-  const_entry_boxed  : bool }
+  const_entry_opaque : bool }
 
 type parameter_entry = types * bool  (*inline flag*)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 078d70965d..f26d49dde4 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -190,8 +190,8 @@ type unsafe_type_judgment = {
 (** {6 Compilation of global declaration } *)
 
 val compile_constant_body :
-    env -> constr_substituted option -> bool -> bool -> Cemitcodes.body_code
-                                 (** opaque *) (* boxed *)
+    env -> constr_substituted option -> bool -> Cemitcodes.body_code
+                                 (** opaque *)
 
 exception Hyp_not_found
 
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 5a3dade530..407ae73ca7 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -95,7 +95,7 @@ and check_with_aux_def env sign with_decl mp equiv =
 			let cb' = {cb with
 				     const_body = body;
 				     const_body_code = Cemitcodes.from_val
-                            (compile_constant_body env' body false false);
+                            (compile_constant_body env' body false);
                                      const_constraints = cst} in
 			  SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
 		    | Some b ->
@@ -105,7 +105,7 @@ and check_with_aux_def env sign with_decl mp equiv =
 			let cb' = {cb with
 				     const_body = body;
 				     const_body_code = Cemitcodes.from_val
-                            (compile_constant_body env' body false false);
+                            (compile_constant_body env' body false);
                                      const_constraints = cst} in
 			  SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
 	      end
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 9da2f49622..ce968b40ef 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -276,7 +276,7 @@ let strengthen_const env mp_from l cb resolver =
 	   const_body = const_subs;
 	   const_opaque = false;
 	   const_body_code = Cemitcodes.from_val
-            (compile_constant_body env const_subs false false)
+            (compile_constant_body env const_subs false)
 	}
 	  
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f765dd77e9..432460d7d5 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -94,11 +94,11 @@ let infer_declaration env dcl =
       let (j,cst) = infer env c.const_entry_body in
       let (typ,cst) = constrain_type env j cst c.const_entry_type in
       Some (Declarations.from_val j.uj_val), typ, cst,
-        c.const_entry_opaque, c.const_entry_boxed, false
+        c.const_entry_opaque, false
   | ParameterEntry (t,nl) ->
       let (j,cst) = infer env t in
       None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst,
-        false, false, nl
+        false, nl
 
 let global_vars_set_constant_type env = function
   | NonPolymorphicType t -> global_vars_set env t
@@ -108,7 +108,7 @@ let global_vars_set_constant_type env = function
 	  (fun t c -> Idset.union (global_vars_set env t) c))
       ctx ~init:Idset.empty
 
-let build_constant_declaration env kn (body,typ,cst,op,boxed,inline) =
+let build_constant_declaration env kn (body,typ,cst,op,inline) =
   let ids =
     match body with
     | None -> global_vars_set_constant_type env typ
@@ -117,7 +117,7 @@ let build_constant_declaration env kn (body,typ,cst,op,boxed,inline) =
 	  (global_vars_set env (Declarations.force b))
 	  (global_vars_set_constant_type env typ)
   in
-  let tps = Cemitcodes.from_val (compile_constant_body env body op boxed) in
+  let tps = Cemitcodes.from_val (compile_constant_body env body op) in
   let hyps = keep_hyps env ids in
     { const_hyps = hyps;
       const_body = body;
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 628aa93756..500858a59c 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -22,10 +22,10 @@ val translate_local_assum : env -> types ->
   types * Univ.constraints
 
 val infer_declaration : env -> constant_entry ->
-   constr_substituted option * constant_type * constraints * bool * bool * bool
+   constr_substituted option * constant_type * constraints * bool * bool
 
 val build_constant_declaration : env -> 'a ->
-    constr_substituted option * constant_type * constraints * bool * bool * bool ->
+    constr_substituted option * constant_type * constraints * bool * bool ->
       constant_body
 
 val translate_constant : env -> constant -> constant_entry -> constant_body