From f19a9d9d3a410fda982b2cf9154da5774f9ec84f Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 28 Jan 2011 13:20:41 +0000
Subject: 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
---
 plugins/funind/functional_principles_types.ml | 4 +---
 plugins/funind/indfun.ml                      | 5 ++---
 plugins/funind/recdef.ml                      | 3 +--
 3 files changed, 4 insertions(+), 8 deletions(-)

(limited to 'plugins/funind')

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) =
-- 
cgit v1.2.3