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 777b33bf9b..aa0357fbb4 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 b2b311a4fd..d141528420 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 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
diff --git a/lib/flags.ml b/lib/flags.ml
index 8ec4a23512..13f5403790 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 7c46686778..ecb4d6dd63 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 5ae048d65e..ba40f98c0d 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 6b03442f54..88ef763c95 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 a9c4630204..fa95fe313c 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 4abc2e5eb1..f6943871c1 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 0583403df0..21281f6e48 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 0cc5af99f2..1d089409b0 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 f23fcd6134..e571803273 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 3ab9d58d50..feff5d67c6 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 f05e003387..e2d8e67e6b 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 9259d490fb..fd5bcd9355 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 fa77099826..5dcd6d840d 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 87b64c8d8f..5845062dd2 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 e009f14eaa..1763d70a62 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 073cd2f63c..e499f22201 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 d157bffce9..41190e8d9a 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 769869584d..6c250ef4f9 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 e805428313..f5d452f7e6 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 9a79f28783..38c65cdd09 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 e614085e48..fbdaa8d3b1 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 0d5f7b86e0..aae5383892 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 794143de49..9098922e31 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 55991c8e88..72549a011e 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 d61ca2bc8b..3d1e836a78 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 cafe454851..3e8c71482a 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 eb33850a7b..57453ac4d7 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 c319801581..95814302d9 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 188bc3dc5f..a6a36672be 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 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 *)
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 53fee9875f..605196d6fc 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 4c2353fc88..242a8e52b4 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 7f5dacaaef..76d8750cb3 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 f5a450a5c9..f11bdb4a8e 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 93b05290fc..c180785d56 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 47387b8c29..163f68fd05 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 6d98d3dd0c..b85c00714f 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 daa93a7e66..51dc1dc30e 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 8d8997a2b4..f7ff2013b7 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 0d7a3b2f96..847278b07a 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 ea11ca487b..27b6ffabe1 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 16817143d8..a18340e904 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 72c9b1fe85..80191b8fda 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