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

1 files changed, 2 insertions, 7 deletions

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 1138031c7..277b343b2 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;