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

18 files changed, 33 insertions, 49 deletions

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