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

71 files changed, 143 insertions, 239 deletions

diff --git a/CHANGES b/CHANGES
index 777b33bf9..aa0357fbb 100644
--- a/CHANGES
+++ b/CHANGES
@@ -17,6 +17,8 @@ Vernacular commands
 - When the output file of "Print Universes" ends in ".dot" or ".gv",
   the universe graph is printed in the DOT language, and can be
   processed by Graphviz tools.
+- The undocumented and obsolete option "Set/Unset Boxed Definitions" has
+  been removed, as well as syntaxes like "Boxed Fixpoint foo".
 
 Libraries
 
diff --git a/Makefile.build b/Makefile.build
index b2b311a4f..d14152842 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -63,14 +63,13 @@ READABLE_ML4=	# non-empty means .ml of .ml4 will be ascii instead of binary
 VALIDATE=
 COQ_XML=	# is "-xml" when building XML library
 VM=		# is "-no-vm" to not use the vm"
-UNBOXEDVALUES=	# is "-unboxed-values" to use unboxed values
 TIMECMD=	# is "'time -p'" to get compilation time of .v
 
 # NB: variable TIME, if set, is the formatting string for unix command 'time'.
 # For instance:
 # TIME="%C (%U user, %S sys, %e total, %M maxres)"
 
-COQOPTS=$(COQ_XML) $(VM) $(UNBOXEDVALUES)
+COQOPTS=$(COQ_XML) $(VM)
 BOOTCOQTOP:=$(TIMECMD) $(BESTCOQTOP) -boot $(COQOPTS)
 
 # The SHOW and HIDE variables control whether make will echo complete commands 
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 9c00af5df..337b90751 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 bf9c0be26..403c1c7b5 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 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;
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index a8ecc82b4..43cebb474 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 e4336683d..d01398841 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 0f604a4be..09b42d0b1 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 983c1f26d..897cbf13a 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 714da0319..dbf802bb1 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 2ba306455..d45e2bbdb 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 078d70965..f26d49dde 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 5a3dade53..407ae73ca 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 9da2f4962..ce968b40e 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 f765dd77e..432460d7d 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 628aa9375..500858a59 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
diff --git a/lib/flags.ml b/lib/flags.ml
index 8ec4a2351..13f540379 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -84,12 +84,6 @@ let unsafe_set = ref Stringset.empty
 let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set
 let is_unsafe s = Stringset.mem s !unsafe_set
 
-(* Flags for the virtual machine *)
-
-let boxed_definitions = ref true
-let set_boxed_definitions b = boxed_definitions := b
-let boxed_definitions _ = !boxed_definitions
-
 (* Flags for external tools *)
 
 let subst_command_placeholder s t =
diff --git a/lib/flags.mli b/lib/flags.mli
index 7c4668677..ecb4d6dd6 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -65,11 +65,6 @@ val print_hyps_limit : unit -> int option
 val add_unsafe : string -> unit
 val is_unsafe : string -> bool
 
-(** Options for the virtual machine *)
-
-val set_boxed_definitions : bool -> unit
-val boxed_definitions : unit -> bool
-
 (** Options for external tools *)
 
 (** Returns string format for default browser to use from Coq or CoqIDE *)
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 5ae048d65..ba40f98c0 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -15,8 +15,6 @@ type locality =
   | Local
   | Global
 
-type boxed_flag = bool
-
 type theorem_kind =
   | Theorem
   | Lemma
@@ -52,7 +50,7 @@ type assumption_object_kind = Definitional | Logical | Conjectural
 *)
 type assumption_kind = locality * assumption_object_kind
 
-type definition_kind = locality * boxed_flag * definition_object_kind
+type definition_kind = locality * definition_object_kind
 
 (* Kinds used in proofs *)
 
@@ -84,12 +82,12 @@ let string_of_theorem_kind = function
   | Proposition -> "Proposition"
   | Corollary -> "Corollary"
 
-let string_of_definition_kind (l,boxed,d) =
-  match (l,d) with
+let string_of_definition_kind def =
+  match def with
   | Local, Coercion -> "Coercion Local"
   | Global, Coercion -> "Coercion"
   | Local, Definition -> "Let"
-  | Global, Definition -> if boxed then "Boxed Definition" else "Definition"
+  | Global, Definition -> "Definition"
   | Local, SubClass -> "Local SubClass"
   | Global, SubClass -> "SubClass"
   | Global, CanonicalStructure -> "Canonical Structure"
diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli
index 6b03442f5..88ef763c9 100644
--- a/library/decl_kinds.mli
+++ b/library/decl_kinds.mli
@@ -15,8 +15,6 @@ type locality =
   | Local
   | Global
 
-type boxed_flag = bool
-
 type theorem_kind =
   | Theorem
   | Lemma
@@ -52,7 +50,7 @@ type assumption_object_kind = Definitional | Logical | Conjectural
 *)
 type assumption_kind = locality * assumption_object_kind
 
-type definition_kind = locality * boxed_flag * definition_object_kind
+type definition_kind = locality * definition_object_kind
 
 (** Kinds used in proofs *)
 
@@ -74,7 +72,7 @@ type logical_kind =
 val logical_kind_of_goal_kind : goal_object_kind -> logical_kind
 val string_of_theorem_kind : theorem_kind -> string
 val string_of_definition_kind :
-  locality * boxed_flag * definition_object_kind -> string
+  locality * definition_object_kind -> string
 
 (** About locality *)
 
diff --git a/library/declare.ml b/library/declare.ml
index a9c463020..fa95fe313 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -160,8 +160,7 @@ let hcons_constant_declaration = function
       DefinitionEntry
        { const_entry_body = hcons1_constr ce.const_entry_body;
 	 const_entry_type = Option.map hcons1_constr ce.const_entry_type;
-         const_entry_opaque = ce.const_entry_opaque;
-         const_entry_boxed = ce.const_entry_boxed }
+         const_entry_opaque = ce.const_entry_opaque }
   | cd -> cd
 
 let declare_constant_common id dhyps (cd,kind) =
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4abc2e5eb..f6943871c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -152,10 +152,6 @@ GEXTEND Gram
       | stre = assumptions_token; nl = inline; bl = assum_list ->
 	  test_plurial_form bl;
 	  VernacAssumption (stre, nl, bl)
-      | IDENT "Boxed";"Definition";id = identref; b = def_body ->
-	  VernacDefinition ((Global,true,Definition), id, b, no_hook)
-      | IDENT "Unboxed";"Definition";id = identref; b = def_body ->
-	  VernacDefinition ((Global,false,Definition), id, b, no_hook)
       | (f,d) = def_token; id = identref; b = def_body ->
           VernacDefinition (d, id, b, f)
       (* Gallina inductive declarations *)
@@ -164,14 +160,10 @@ GEXTEND Gram
 	  let (k,f) = f in
 	  let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
           VernacInductive (f,false,indl)
-      | IDENT "Boxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint (recs,true)
-      | IDENT "Unboxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint (recs,false)
-       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint (recs,Flags.boxed_definitions())
+      | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+          VernacFixpoint recs
       | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint (corecs,false)
+          VernacCoFixpoint corecs
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l
       | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
 	l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) ] ]
@@ -201,13 +193,13 @@ GEXTEND Gram
   ;
   def_token:
     [ [ "Definition" ->
-	no_hook, (Global, Flags.boxed_definitions(), Definition)
+	no_hook, (Global, Definition)
       | IDENT "Let" ->
-	no_hook, (Local, Flags.boxed_definitions(), Definition)
+	no_hook, (Local, Definition)
       | IDENT "Example" ->
-	no_hook, (Global, Flags.boxed_definitions(), Example)
+	no_hook, (Global, Example)
       | IDENT "SubClass"  ->
-          Class.add_subclass_hook, (use_locality_exp (), false, SubClass) ] ]
+          Class.add_subclass_hook, (use_locality_exp (), SubClass) ] ]
   ;
   assumption_token:
     [ [ "Hypothesis" -> (Local, Logical)
@@ -510,16 +502,16 @@ GEXTEND Gram
           d = def_body ->
           let s = coerce_reference_to_id qid in
 	  VernacDefinition
-	    ((Global,false,CanonicalStructure),(dummy_loc,s),d,
+	    ((Global,CanonicalStructure),(dummy_loc,s),d,
 	     (fun _ -> Recordops.declare_canonical_structure))
 
       (* Coercions *)
       | IDENT "Coercion"; qid = global; d = def_body ->
           let s = coerce_reference_to_id qid in
-	  VernacDefinition ((use_locality_exp (),false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+	  VernacDefinition ((use_locality_exp (),Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
       | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body ->
            let s = coerce_reference_to_id qid in
-	  VernacDefinition ((enforce_locality_exp true,false,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
+	  VernacDefinition ((enforce_locality_exp true,Coercion),(dummy_loc,s),d,Class.add_coercion_hook)
       | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref;
          ":"; s = class_rawexpr; ">->"; t = class_rawexpr ->
 	   VernacIdentityCoercion (enforce_locality_exp true, f, s, t)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 0583403df..21281f6e4 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -607,7 +607,7 @@ let rec pr_vernac = function
       (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
 
 
-  | VernacFixpoint (recs,b) ->
+  | VernacFixpoint recs ->
       let pr_onerec = function
         | ((loc,id),ro,bl,type_,def),ntn ->
             let annot = pr_guard_annot bl ro in
@@ -616,19 +616,17 @@ let rec pr_vernac = function
             ++ pr_opt (fun def -> str" :=" ++ brk(1,2) ++ pr_lconstr def) def ++
 	    prlist (pr_decl_notation pr_constr) ntn
       in
-      let start = if b then "Boxed Fixpoint" else "Fixpoint" in
-      hov 0 (str start ++ spc() ++
+      hov 0 (str "Fixpoint" ++ spc() ++
         prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs)
 
-  | VernacCoFixpoint (corecs,b) ->
+  | VernacCoFixpoint corecs ->
       let pr_onecorec (((loc,id),bl,c,def),ntn) =
         pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
         spc() ++ pr_lconstr_expr c ++
         pr_opt (fun def -> str" :=" ++ brk(1,2) ++ pr_lconstr def) def ++
 	prlist (pr_decl_notation pr_constr) ntn
       in
-      let start = if b then "Boxed CoFixpoint" else "CoFixpoint" in
-      hov 0 (str start ++ spc() ++
+      hov 0 (str "CoFixpoint" ++ spc() ++
       prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs)
   | VernacScheme l ->
       hov 2 (str"Scheme" ++ spc() ++
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 0cc5af99f..1d089409b 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -382,9 +382,7 @@ let generate_functional_principle
 	let ce =
 	  { const_entry_body = value;
 	    const_entry_type = None;
-	    const_entry_opaque = false;
-	    const_entry_boxed = Flags.boxed_definitions()
-	  }
+	    const_entry_opaque = false }
 	in
 	ignore(
 	  Declare.declare_constant
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f23fcd613..e57180327 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -351,14 +351,13 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
     | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err_loc (dummy_loc,"Function",str "Body of Function must be given") in 
 	let ce,imps =
-	  Command.interp_definition
-	    (Flags.boxed_definitions ()) bl None body (Some ret_type)
+	  Command.interp_definition bl None body (Some ret_type)
 	in
 	Command.declare_definition
 	  fname (Decl_kinds.Global,Decl_kinds.Definition)
 	  ce imps (fun _ _ -> ())
     | _ ->
-	Command.do_fixpoint fixpoint_exprl (Flags.boxed_definitions())
+	Command.do_fixpoint fixpoint_exprl
 
 let generate_correction_proof_wf f_ref tcc_lemma_ref
     is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 3ab9d58d5..feff5d67c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1136,8 +1136,7 @@ let (declare_fun : identifier -> logical_kind -> constr -> global_reference) =
   fun f_id kind value ->
     let ce = {const_entry_body = value;
 	      const_entry_type = None;
-	      const_entry_opaque = false;
-              const_entry_boxed = true} in
+	      const_entry_opaque = false } in
       ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
 
 let (declare_f : identifier -> logical_kind -> constr list -> global_reference -> global_reference) =
diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v
index f05e00338..e2d8e67e6 100644
--- a/plugins/quote/Quote.v
+++ b/plugins/quote/Quote.v
@@ -26,7 +26,6 @@ Declare ML Module "quote_plugin".
 ***********************************************************************)
 
 Set Implicit Arguments.
-Unset Boxed Definitions.
 
 Section variables_map.
 
diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v
index 9259d490f..fd5bcd935 100644
--- a/plugins/ring/LegacyArithRing.v
+++ b/plugins/ring/LegacyArithRing.v
@@ -15,7 +15,7 @@ Require Import Eqdep_dec.
 
 Open Local Scope nat_scope.
 
-Unboxed Fixpoint nateq (n m:nat) {struct m} : bool :=
+Fixpoint nateq (n m:nat) {struct m} : bool :=
   match n, m with
   | O, O => true
   | S n', S m' => nateq n' m'
diff --git a/plugins/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v
index fa7709982..5dcd6d840 100644
--- a/plugins/ring/LegacyNArithRing.v
+++ b/plugins/ring/LegacyNArithRing.v
@@ -14,7 +14,7 @@ Require Export ZArith_base.
 Require Import NArith.
 Require Import Eqdep_dec.
 
-Unboxed Definition Neq (n m:N) :=
+Definition Neq (n m:N) :=
   match (n ?= m)%N with
   | Datatypes.Eq => true
   | _ => false
diff --git a/plugins/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v
index 87b64c8d8..5845062dd 100644
--- a/plugins/ring/LegacyZArithRing.v
+++ b/plugins/ring/LegacyZArithRing.v
@@ -13,7 +13,7 @@ Require Export ZArith_base.
 Require Import Eqdep_dec.
 Require Import LegacyRing.
 
-Unboxed Definition Zeq (x y:Z) :=
+Definition Zeq (x y:Z) :=
   match (x ?= y)%Z with
   | Datatypes.Eq => true
   | _ => false
diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v
index e009f14ea..1763d70a6 100644
--- a/plugins/ring/Ring_abstract.v
+++ b/plugins/ring/Ring_abstract.v
@@ -10,8 +10,6 @@ Require Import LegacyRing_theory.
 Require Import Quote.
 Require Import Ring_normalize.
 
-Unset Boxed Definitions.
-
 Section abstract_semi_rings.
 
 Inductive aspolynomial : Type :=
diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v
index 073cd2f63..e499f2220 100644
--- a/plugins/ring/Ring_normalize.v
+++ b/plugins/ring/Ring_normalize.v
@@ -10,7 +10,6 @@ Require Import LegacyRing_theory.
 Require Import Quote.
 
 Set Implicit Arguments.
-Unset Boxed Definitions.
 
 Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m.
 Proof.
diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v
index d157bffce..41190e8d9 100644
--- a/plugins/ring/Setoid_ring_normalize.v
+++ b/plugins/ring/Setoid_ring_normalize.v
@@ -10,7 +10,6 @@ Require Import Setoid_ring_theory.
 Require Import Quote.
 
 Set Implicit Arguments.
-Unset Boxed Definitions.
 
 Lemma index_eq_prop : forall n m:index, Is_true (index_eq n m) -> n = m.
 Proof.
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 769869584..6c250ef4f 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -9,8 +9,6 @@
 Require Export List.
 Require Export BinPos.
 
-Unset Boxed Definitions.
-
 Open Scope positive_scope.
 
 Ltac clean := try (simpl; congruence).
diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v
index e80542831..f5d452f7e 100644
--- a/plugins/rtauto/Rtauto.v
+++ b/plugins/rtauto/Rtauto.v
@@ -10,7 +10,6 @@
 Require Export List.
 Require Export Bintree.
 Require Import Bool.
-Unset Boxed Definitions.
 
 Declare ML Module "rtauto_plugin".
 
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 9a79f2878..38c65cdd0 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -159,8 +159,7 @@ let decl_constant na c =
   mkConst(declare_constant (id_of_string na) (DefinitionEntry
     { const_entry_body = c;
       const_entry_type = None;
-      const_entry_opaque = true;
-      const_entry_boxed = true},
+      const_entry_opaque = true },
     IsProof Lemma))
 
 (* Calling a global tactic *)
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index e614085e4..fbdaa8d3b 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -141,12 +141,12 @@ let subtac (loc, command) =
 	    (fun _ _ -> ())
       | DefineBody (bl, _, c, tycon) ->
 	  ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon))
-  | VernacFixpoint (l, b) ->
+  | VernacFixpoint l ->
       List.iter (fun ((lid, _, _, _, _), _) ->
 	check_fresh lid;
 	Dumpglob.dump_definition lid false "fix") l;
       let _ = trace (str "Building fixpoint") in
-	ignore(Subtac_command.build_recursive l b)
+	ignore(Subtac_command.build_recursive l)
 
   | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) ->
       if guard <> None then 
@@ -171,10 +171,10 @@ let subtac (loc, command) =
 	error "Declare Instance not supported here.";
       ignore(Subtac_classes.new_instance ~global:glob sup is props pri)
 
-  | VernacCoFixpoint (l, b) ->
+  | VernacCoFixpoint l ->
       if Dumpglob.dump () then
 	List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l;
-      ignore(Subtac_command.build_corecursive l b)
+      ignore(Subtac_command.build_corecursive l)
 
   (*| VernacEndProof e ->
     subtac_end_proof e*)
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 0d5f7b86e..aae538389 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -176,4 +176,4 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
   in
   let evm = Subtac_utils.evars_of_term !evars Evd.empty term in
   let obls, _, constr, typ = Eterm.eterm_obligations env id !evars evm 0 term termtype in
-    id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,false,Instance) ~hook obls
+    id, Subtac_obligations.add_definition id ~term:constr typ ~kind:(Global,Instance) ~hook obls
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 794143de4..9098922e3 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -215,7 +215,7 @@ let nf_evar_context isevars ctx =
   List.map (fun (n, b, t) ->
     (n, Option.map (Evarutil.nf_evar isevars) b, Evarutil.nf_evar isevars t)) ctx
 
-let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
+let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let sigma = Evd.empty in
   let isevars = ref (Evd.create_evar_defs sigma) in
@@ -327,8 +327,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
 	let ce =
 	  { const_entry_body = Evarutil.nf_evar !isevars body;
 	    const_entry_type = Some ty;
-	    const_entry_opaque = false;
-	    const_entry_boxed = false} 
+	    const_entry_opaque = false }
 	in 
 	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
 	let gr = ConstRef c in
@@ -417,7 +416,7 @@ let out_def = function
   | Some def -> def
   | None -> error "Program Fixpoint needs defined bodies."
 
-let interp_recursive fixkind l boxed =
+let interp_recursive fixkind l =
   let env = Global.env() in
   let fixl, ntnl = List.split l in
   let kind = fixkind <> IsCoFixpoint in
@@ -506,7 +505,7 @@ let out_n = function
     Some n -> n
   | None -> raise Not_found
 
-let build_recursive l b =
+let build_recursive l =
   let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
     match g, l with
 	[(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
@@ -514,24 +513,24 @@ let build_recursive l b =
 		    (match n with Some n -> mkIdentC (snd n) | None ->
 		      errorlabstrm "Subtac_command.build_recursive"
 			(str "Recursive argument required for well-founded fixpoints"))
-		    ntn false)
+		    ntn)
 
       | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] ->
 	  ignore(build_wellfounded (id, n, bl, typ, out_def def) (Option.default (CRef lt_ref) r)
-		    m ntn false)
+		    m ntn)
 
       | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
 	  let fixl = List.map (fun (((_,id),(n,ro),bl,typ,def),ntn) ->
 	    ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = n;
 	      Command.fix_body = def; Command.fix_type = typ},ntn)) l
-	  in interp_recursive (IsFixpoint g) fixl b
+	  in interp_recursive (IsFixpoint g) fixl
       | _, _ ->
 	  errorlabstrm "Subtac_command.build_recursive"
 	    (str "Well-founded fixpoints not allowed in mutually recursive blocks")
 
-let build_corecursive l b =
+let build_corecursive l =
   let fixl = List.map (fun (((_,id),bl,typ,def),ntn) ->
     ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = None;
       Command.fix_body = def; Command.fix_type = typ},ntn))
     l in
-  interp_recursive IsCoFixpoint fixl b
+  interp_recursive IsCoFixpoint fixl
diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli
index 55991c8e8..72549a011 100644
--- a/plugins/subtac/subtac_command.mli
+++ b/plugins/subtac/subtac_command.mli
@@ -51,10 +51,10 @@ val build_wellfounded :
            Names.identifier * 'a * Topconstr.local_binder list *
            Topconstr.constr_expr * Topconstr.constr_expr ->
            Topconstr.constr_expr ->
-           Topconstr.constr_expr -> 'b -> 'c -> Subtac_obligations.progress
+           Topconstr.constr_expr -> 'b -> Subtac_obligations.progress
 
 val build_recursive :
-  (fixpoint_expr * decl_notation list) list -> bool -> unit
+  (fixpoint_expr * decl_notation list) list -> unit
 
 val build_corecursive :
-  (cofixpoint_expr * decl_notation list) list -> bool -> unit
+  (cofixpoint_expr * decl_notation list) list -> unit
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index d61ca2bc8..3d1e836a7 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -184,12 +184,11 @@ let declare_definition prg =
 		  my_print_constr (Global.env()) body ++ str " : " ++
 		  my_print_constr (Global.env()) prg.prg_type);
      with _ -> ());
-  let (local, boxed, kind) = prg.prg_kind in
+  let (local, kind) = prg.prg_kind in
   let ce =
     { const_entry_body = body;
       const_entry_type = Some typ;
-      const_entry_opaque = false;
-      const_entry_boxed = boxed}
+      const_entry_opaque = false }
   in
     (Command.get_declare_definition_hook ()) ce;
     match local with
@@ -207,7 +206,7 @@ let declare_definition prg =
     | (Global|Local) ->
 	let c =
 	  Declare.declare_constant
-	    prg.prg_name (DefinitionEntry ce,IsDefinition (pi3 prg.prg_kind))
+	    prg.prg_name (DefinitionEntry ce,IsDefinition (snd prg.prg_kind))
 	in
 	let gr = ConstRef c in
 	  if Impargs.is_implicit_args () || prg.prg_implicits <> [] then
@@ -255,7 +254,7 @@ let declare_mutual_definition l =
   let fixkind = Option.get first.prg_fixkind in
   let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
   let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
-  let (local,boxed,kind) = first.prg_kind in
+  let (local,kind) = first.prg_kind in
   let fixnames = first.prg_deps in
   let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
   let indexes, fixdecls =
@@ -269,7 +268,7 @@ let declare_mutual_definition l =
 	  None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l
   in
   (* Declare the recursive definitions *)
-  let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in
+  let kns = list_map4 (declare_fix kind) fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
     List.iter Metasyntax.add_notation_interpretation first.prg_notations;
     Declare.recursive_message (fixkind<>IsCoFixpoint) indexes fixnames;
@@ -288,8 +287,7 @@ let declare_obligation prg obl body =
       let ce = 
 	{ const_entry_body = body;
 	  const_entry_type = Some ty;
-	  const_entry_opaque = opaque;
-	  const_entry_boxed = false} 
+	  const_entry_opaque = opaque }
       in
       let constant = Declare.declare_constant obl.obl_name
 	(DefinitionEntry ce,IsProof Property)
@@ -557,7 +555,7 @@ let show_term n =
 	      my_print_constr (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ my_print_constr (Global.env ()) prg.prg_body)
 
-let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
     ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
   Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
   let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
@@ -575,7 +573,7 @@ let add_definition n ?term t ?(implicits=[]) ?(kind=Global,false,Definition) ?ta
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	| _ -> res)
 
-let add_mutual_definitions l ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) 
+let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce)
     ?(hook=fun _ _ -> ()) notations fixkind =
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
   let upd = List.fold_left
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index cafe45485..3e8c71482 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -265,11 +265,11 @@ let close_proof () =
     let id = get_current_proof_name () in
     let p = give_me_the_proof () in
     let proofs_and_types = Proof.return p in
-    let entries = List.map (fun (c,t) -> { Entries.const_entry_body = c ;
-                                    					   const_entry_type  = Some t;
-									   const_entry_opaque = true ;
-									   const_entry_boxed = false } )
-                                         proofs_and_types 
+    let entries = List.map
+      (fun (c,t) -> { Entries.const_entry_body = c ;
+                      const_entry_type  = Some t;
+		      const_entry_opaque = true })
+      proofs_and_types
     in
     let { compute_guard=cg ; strength=str ; hook=hook } =
       Idmap.find id !proof_info
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index eb33850a7..57453ac4d 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -147,12 +147,10 @@ let parse_args () =
     | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
 
     | ("-notactics"|"-debug"|"-nolib"
-      |"-debugVM"|"-alltransp"|"-VMno"
       |"-batch"|"-nois"|"-noglob"|"-no-glob"
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
       |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
-      |"-dont-load-proofs"|"-load-proofs"|"-impredicative-set"|"-vm"
-      |"-unboxed-values"|"-unboxed-definitions"|"-draw-vm-instr" as o) :: rem ->
+      |"-dont-load-proofs"|"-load-proofs"|"-impredicative-set"|"-vm" as o) :: rem ->
 	parse (cfiles,o::args) rem
 
     | ("-where") :: _ ->
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index c31980158..95814302d 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -236,8 +236,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
     (DefinitionEntry
        { const_entry_body = invProof;
          const_entry_type = None;
-         const_entry_opaque = false;
-	 const_entry_boxed = true && (Flags.boxed_definitions())},
+         const_entry_opaque = false },
      IsProof Lemma)
   in ()
 
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 188bc3dc5..a6a36672b 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1345,8 +1345,7 @@ let declare_projection n instance_id r =
   let cst =
     { const_entry_body = term;
       const_entry_type = Some typ;
-      const_entry_opaque = false;
-      const_entry_boxed = false }
+      const_entry_opaque = false }
   in
     ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
 
diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v
index fd902aa84..1dd5ce16c 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 216ca35af..03487b6d6 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 81e2e06e4..686a0692c 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 97d935e4f..d2e6c70b9 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 0ffce766c..64e32c560 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 cbf6da197..e858d2148 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 525eff688..1eee8d852 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 0687bfbc2..d16e7f2c7 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 76d66ca06..12258d6b5 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 5f8b5d9da..479d381d4 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 2fdf1ffea..8c46f355f 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 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 *)
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 53fee9875..605196d6f 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -29,7 +29,7 @@ let build_table l =
 
 let is_keyword =
   build_table
-    [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint";
+    [ "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "CoFixpoint";
       "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example";
       "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
       "Hypothesis"; "Hypotheses";
@@ -41,8 +41,7 @@ let is_keyword =
       "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
       "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
       "Notation"; "Reserved Notation"; "Tactic Notation";
-      "Delimit"; "Bind"; "Open"; "Scope";
-      "Boxed"; "Unboxed"; "Inline";
+      "Delimit"; "Bind"; "Open"; "Scope"; "Inline";
       "Implicit Arguments"; "Add"; "Strict";
       "Typeclasses"; "Instance"; "Global Instance"; "Class"; "Instantiation";
       "subgoal";
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 4c2353fc8..242a8e52b 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -179,8 +179,9 @@ let declare_record_instance gr ctx params =
   let ident = make_instance_ident gr in
   let def = it_mkLambda_or_LetIn (applistc (constr_of_global gr) params) ctx in
   let def = deep_refresh_universes def in
-  let ce = { const_entry_body=def; const_entry_type=None;
-	     const_entry_opaque=false; const_entry_boxed=false } in
+  let ce = { const_entry_body=def;
+	     const_entry_type=None;
+	     const_entry_opaque=false } in
   let cst = Declare.declare_constant ident
     (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in
   new_instance_message ident (Typeops.type_of_constant (Global.env()) cst) def
@@ -193,8 +194,9 @@ let declare_class_instance gr ctx params =
   let def = deep_refresh_universes def in
   let typ = deep_refresh_universes typ in
   let ce = Entries.DefinitionEntry
-    {  const_entry_type=Some typ; const_entry_body=def;
-       const_entry_opaque=false; const_entry_boxed=false } in
+    {  const_entry_type=Some typ;
+       const_entry_body=def;
+       const_entry_opaque=false } in
   try
   let cst = Declare.declare_constant ident
     (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 7f5dacaae..76d8750cb 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -218,8 +218,7 @@ let build_id_coercion idf_opt source =
     DefinitionEntry
       { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f);
 	const_entry_type = Some typ_f;
-        const_entry_opaque = false;
-	const_entry_boxed = Flags.boxed_definitions()} in
+        const_entry_opaque = false } in
   let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in
   ConstRef kn
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index f5a450a5c..f11bdb4a8 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -108,8 +108,7 @@ let declare_instance_constant k pri global imps ?hook id term termtype =
     let entry =
       { const_entry_body   = term;
 	const_entry_type   = Some termtype;
-	const_entry_opaque = false;
-	const_entry_boxed  = false }
+	const_entry_opaque = false }
     in DefinitionEntry entry, kind
   in
   let kn = Declare.declare_constant id cdecl in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 93b05290f..c180785d5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -64,7 +64,7 @@ let red_constant_entry n ce = function
       { ce with const_entry_body =
 	under_binders (Global.env()) (fst (reduction_of_red_expr red)) n body }
 
-let interp_definition boxed bl red_option c ctypopt =
+let interp_definition bl red_option c ctypopt =
   let env = Global.env() in
   let evdref = ref Evd.empty in
   let (env_bl, ctx), imps1 = interp_context_evars evdref env bl in
@@ -77,8 +77,7 @@ let interp_definition boxed bl red_option c ctypopt =
 	imps1@imps2,
 	{ const_entry_body = body;
 	  const_entry_type = None;
-          const_entry_opaque = false;
-	  const_entry_boxed = boxed }
+          const_entry_opaque = false }
     | Some ctyp ->
 	let ty, impls = interp_type_evars_impls ~evdref ~fail_evar:false env_bl ctyp in
 	let c, imps2 = interp_casted_constr_evars_impls ~evdref ~fail_evar:false env_bl c ty in
@@ -89,8 +88,7 @@ let interp_definition boxed bl red_option c ctypopt =
 	imps1@imps2,
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;
-          const_entry_opaque = false;
-	  const_entry_boxed = boxed }
+          const_entry_opaque = false }
   in
   red_constant_entry (rel_context_length ctx) ce red_option, imps
 
@@ -469,13 +467,12 @@ let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
-let declare_fix boxed kind f def t imps =
+let declare_fix kind f def t imps =
   let ce = {
     const_entry_body = def;
     const_entry_type = Some t;
-    const_entry_opaque = false;
-    const_entry_boxed = boxed
-  } in
+    const_entry_opaque = false }
+  in
   let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
   let gr = ConstRef kn in
   Autoinstance.search_declaration (ConstRef kn);
@@ -545,7 +542,7 @@ let interp_recursive isfix fixl notations =
 let interp_fixpoint = interp_recursive true
 let interp_cofixpoint = interp_recursive false
 
-let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
+let declare_fixpoint ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
   if List.mem None fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -563,14 +560,14 @@ let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns =
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
     let fixdecls =
       list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
-    ignore (list_map4 (declare_fix boxed Fixpoint) fixnames fixdecls fixtypes fiximps);
+    ignore (list_map4 (declare_fix Fixpoint) fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     fixpoint_message (Some indexes) fixnames;
   end;
   (* Declare notations *)
   List.iter Metasyntax.add_notation_interpretation ntns
 
-let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns =
+let declare_cofixpoint ((fixnames,fixdefs,fixtypes),fiximps) ntns =
   if List.mem None fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -586,7 +583,7 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns =
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let fixdecls = list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
-    ignore (list_map4 (declare_fix boxed CoFixpoint) fixnames fixdecls fixtypes fiximps);
+    ignore (list_map4 (declare_fix CoFixpoint) fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
   end;
@@ -612,13 +609,13 @@ let extract_cofixpoint_components l =
     {fix_name = id; fix_annot = None; fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
   List.flatten ntnl
 
-let do_fixpoint l b =
+let do_fixpoint l =
   let fixl,ntns = extract_fixpoint_components true l in
   let fix = interp_fixpoint fixl ntns in
   let possible_indexes =
     List.map compute_possible_guardness_evidences (snd fix) in
-  declare_fixpoint b fix possible_indexes ntns
+  declare_fixpoint fix possible_indexes ntns
 
-let do_cofixpoint l b =
+let do_cofixpoint l =
   let fixl,ntns = extract_cofixpoint_components l in
-  declare_cofixpoint b (interp_cofixpoint fixl ntns) ntns
+  declare_cofixpoint (interp_cofixpoint fixl ntns) ntns
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 47387b8c2..163f68fd0 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -31,7 +31,7 @@ val set_declare_assumptions_hook : (types -> unit) -> unit
 (** {6 Definitions/Let} *)
 
 val interp_definition :
-  boxed_flag -> local_binder list -> red_expr option -> constr_expr ->
+  local_binder list -> red_expr option -> constr_expr ->
   constr_expr option -> definition_entry * manual_implicits
 
 val declare_definition : identifier -> locality * definition_object_kind ->
@@ -127,26 +127,24 @@ val interp_cofixpoint :
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
-  bool ->
   recursive_preentry * (name list * manual_implicits * int option) list -> 
   lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint :
-  bool ->
   recursive_preentry * (name list * manual_implicits * int option) list ->
     decl_notation list -> unit
 
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint :
-  (fixpoint_expr * decl_notation list) list -> bool -> unit
+  (fixpoint_expr * decl_notation list) list -> unit
 
 val do_cofixpoint :
-  (cofixpoint_expr * decl_notation list) list -> bool -> unit
+  (cofixpoint_expr * decl_notation list) list -> unit
 
 (** Utils *)
 
 val check_mutuality : Environ.env -> bool -> (identifier * types) list -> unit
 
-val declare_fix : bool -> definition_object_kind -> identifier ->
+val declare_fix : definition_object_kind -> identifier ->
   constr -> types -> Impargs.manual_explicitation list -> global_reference
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 6d98d3dd0..b85c00714 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -128,12 +128,10 @@ let set_compat_version = function
 (*s options for the virtual machine *)
 
 let boxed_val = ref false
-let boxed_def = ref false
 let use_vm = ref false
 
 let set_vm_opt () =
   Vm.set_transp_values (not !boxed_val);
-  Flags.set_boxed_definitions !boxed_def;
   Vconv.set_use_vm !use_vm
 
 (*s Parsing of the command line.
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index daa93a7e6..51dc1dc30 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -115,8 +115,7 @@ let define internal id c =
     (DefinitionEntry
       { const_entry_body = c;
         const_entry_type = None;
-        const_entry_opaque = false;
-	const_entry_boxed = Flags.boxed_definitions() },
+        const_entry_opaque = false },
       Decl_kinds.IsDefinition Scheme) in
   (match internal with
   | KernelSilent -> ()
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 8d8997a2b..f7ff2013b 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -105,8 +105,7 @@ let define id internal c t =
     (DefinitionEntry
       { const_entry_body = c;
         const_entry_type = t;
-        const_entry_opaque = false;
-	const_entry_boxed = Flags.boxed_definitions() },
+        const_entry_opaque = false },
       Decl_kinds.IsDefinition Scheme) in
   definition_message id;
   kn
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 0d7a3b2f9..847278b07 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -216,8 +216,7 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
           let const =
             { const_entry_body = body_i;
               const_entry_type = Some t_i;
-              const_entry_opaque = opaq;
-              const_entry_boxed = false (* copy of what cook_proof does *)} in
+              const_entry_opaque = opaq } in
           let kn = declare_constant id (DefinitionEntry const, k) in
           (Global,ConstRef kn,imps)
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index ea11ca487..27b6ffabe 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -201,8 +201,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
 		  let cie = {
 		    const_entry_body = proj;
                     const_entry_type = Some projtyp;
-                    const_entry_opaque = false;
-		    const_entry_boxed = Flags.boxed_definitions() } in
+                    const_entry_opaque = false } in
 		  let k = (DefinitionEntry cie,IsDefinition kind) in
 		  let kn = declare_constant ~internal:KernelSilent fid k in
 		  Flags.if_verbose message (string_of_id fid ^" is defined");
@@ -311,8 +310,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	let class_entry =
 	  { const_entry_body = class_body;
 	    const_entry_type = class_type;
-	    const_entry_opaque = false;
-	    const_entry_boxed = false }
+	    const_entry_opaque = false }
 	in
 	let cst = Declare.declare_constant (snd id)
 	  (DefinitionEntry class_entry, IsDefinition Definition)
@@ -323,8 +321,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	let proj_entry =
 	  { const_entry_body = proj_body;
 	    const_entry_type = Some proj_type;
-	    const_entry_opaque = false;
-	    const_entry_boxed = false }
+	    const_entry_opaque = false }
 	in
 	let proj_cst = Declare.declare_constant proj_name
 	  (DefinitionEntry proj_entry, IsDefinition Definition)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 16817143d..a18340e90 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -328,7 +328,7 @@ let start_proof_and_print k l hook =
   print_subgoals ();
   if !pcoq <> None then (Option.get !pcoq).start_proof ()
 
-let vernac_definition (local,boxed,k) (loc,id as lid) def hook =
+let vernac_definition (local,k) (loc,id as lid) def hook =
   if local = Local then Dumpglob.dump_definition lid true "var"
   else Dumpglob.dump_definition lid false "def";
   (match def with
@@ -342,7 +342,7 @@ let vernac_definition (local,boxed,k) (loc,id as lid) def hook =
           | Some r ->
 	      let (evc,env)= get_current_context () in
  		Some (interp_redexp env evc r) in
-	let ce,imps = interp_definition boxed bl red_option c typ_opt in
+	let ce,imps = interp_definition bl red_option c typ_opt in
 	declare_definition id (local,k) ce imps hook)
 
 let vernac_start_proof kind l lettop hook =
@@ -433,15 +433,15 @@ let vernac_inductive finite infer indl =
     let indl = List.map unpack indl in
     do_mutual_inductive indl (recursivity_flag_of_kind finite)
 
-let vernac_fixpoint l b =
+let vernac_fixpoint l =
   if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  do_fixpoint l b
+  do_fixpoint l
 
-let vernac_cofixpoint l b =
+let vernac_cofixpoint l =
   if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  do_cofixpoint l b
+  do_cofixpoint l
 
 let vernac_scheme = Indschemes.do_scheme
 
@@ -943,14 +943,6 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
-      optname  = "use of boxed definitions";
-      optkey   = ["Boxed";"Definitions"];
-      optread  = Flags.boxed_definitions;
-      optwrite = (fun b -> Flags.set_boxed_definitions b) }
-
-let _ =
-  declare_bool_option
-    { optsync  = true;
       optname  = "use of boxed values";
       optkey   = ["Boxed";"Values"];
       optread  = (fun _ -> not (Vm.transp_values ()));
@@ -1338,8 +1330,8 @@ let interp c = match c with
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption stre l nl
   | VernacInductive (finite,infer,l) -> vernac_inductive finite infer l
-  | VernacFixpoint (l,b) -> vernac_fixpoint l b
-  | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b
+  | VernacFixpoint l -> vernac_fixpoint l
+  | VernacCoFixpoint l -> vernac_cofixpoint l
   | VernacScheme l -> vernac_scheme l
   | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 72c9b1fe8..80191b8fd 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -228,8 +228,8 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of assumption_kind * bool * simple_binder with_coercion list
   | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list
-  | VernacFixpoint of (fixpoint_expr * decl_notation list) list * bool
-  | VernacCoFixpoint of (cofixpoint_expr * decl_notation list) list * bool
+  | VernacFixpoint of (fixpoint_expr * decl_notation list) list
+  | VernacCoFixpoint of (cofixpoint_expr * decl_notation list) list
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list