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

2 files changed, 14 insertions, 24 deletions

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() ++