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

12 files changed, 42 insertions, 63 deletions

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