Changement dans les boxed values .

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 30 insertions, 10 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 43e6b81cc..d09e167b1 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -111,8 +111,13 @@ GEXTEND Gram
   def_token:
     [ [ IDENT "Boxed";"Definition" ->
 	 (fun _ _ -> ()), (Global, Definition true)
-      | "Definition" -> (fun _ _ -> ()), (Global, Definition false)
-      | IDENT "Local" -> (fun _ _ -> ()), (Local, Definition true)
+      | IDENT "Unboxed";"Definition" ->
+	 (fun _ _ -> ()), (Global, Definition false)
+      | "Definition" -> 
+	(fun _ _ -> ()), (Global, Definition false)
+              (*(Options.boxed_definitions())) *)
+      | IDENT "Local" -> 
+	(fun _ _ -> ()), (Local, Definition (Options.boxed_definitions()))
       | IDENT "SubClass"  -> Class.add_subclass_hook, (Global, SubClass)
       | IDENT "Local"; IDENT "SubClass"  ->
 	  Class.add_subclass_hook, (Local, SubClass) ] ] 
@@ -319,10 +324,16 @@ GEXTEND Gram
           VernacInductive (f,indl)
       | IDENT "Boxed"; "Fixpoint"; recs = specifrec ->
 	 VernacFixpoint (recs,true)
-      | "Fixpoint"; recs = specifrec -> VernacFixpoint (recs,false)
-      | IDENT "Boxed"; "CoFixpoint"; corecs = specifcorec -> 
+      | IDENT "Unboxed"; "Fixpoint"; recs = specifrec ->
+	 VernacFixpoint (recs,false)
+      | "Fixpoint"; recs = specifrec -> 
+	 VernacFixpoint (recs,Options.boxed_definitions())
+(*      | IDENT "Boxed"; "CoFixpoint"; corecs = specifcorec -> 
 	 VernacCoFixpoint (corecs,true)
-      | "CoFixpoint"; corecs = specifcorec -> VernacCoFixpoint (corecs,false)
+      | IDENT "Unboxed"; "CoFixpoint"; corecs = specifcorec -> 
+	 VernacCoFixpoint (corecs,false) *)
+      | "CoFixpoint"; corecs = specifcorec -> 
+	 VernacCoFixpoint (corecs,false (*Options.boxed_definitions()*))
       | IDENT "Scheme"; l = schemes -> VernacScheme l
       | f = finite_token; s = csort; id = identref;
 	indpar = simple_binders_list; ":="; lc = constructor_list -> 
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 9cf0d3a21..45237e101 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -103,6 +103,8 @@ GEXTEND Gram
 	  VernacAssumption (stre, bl)
       | IDENT "Boxed";"Definition";id = identref; b = def_body -> 
 	  VernacDefinition ((Global,Definition true), id, b, (fun _ _ -> ()))
+      | IDENT "Unboxed";"Definition";id = identref; b = def_body -> 
+	  VernacDefinition ((Global,Definition false), id, b, (fun _ _ -> ()))
       | (f,d) = def_token; id = identref; b = def_body -> 
           VernacDefinition (d, id, b, f)
       (* Gallina inductive declarations *)
@@ -111,13 +113,18 @@ GEXTEND Gram
           VernacInductive (f,indl)
       | IDENT "Boxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           VernacFixpoint (recs,true)
-      | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+      | IDENT "Unboxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           VernacFixpoint (recs,false)
-      | IDENT "Boxed"; "CoFixpoint"; 
+       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+          VernacFixpoint (recs,Options.boxed_definitions())
+     (* | IDENT "Boxed"; "CoFixpoint"; 
 	   corecs = LIST1 corec_definition SEP "with" ->
           VernacCoFixpoint (corecs,true)
+      | IDENT "Unboxed"; "CoFixpoint"; 
+	   corecs = LIST1 corec_definition SEP "with" ->
+          VernacCoFixpoint (corecs,false) *)
       | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint (corecs,false)
+          VernacCoFixpoint (corecs,false (*Options.boxed_definitions()*))
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ]
   ;
   gallina_ext:
@@ -140,8 +147,10 @@ GEXTEND Gram
       | IDENT "Remark" -> Remark ] ]
   ;
   def_token:
-    [ [ "Definition" -> (fun _ _ -> ()), (Global, Definition false)
-      | IDENT "Let" -> (fun _ _ -> ()), (Local, Definition false)
+    [ [ "Definition" -> 
+	(fun _ _ -> ()), (Global, Definition (Options.boxed_definitions()))
+      | IDENT "Let" -> 
+	(fun _ _ -> ()), (Local, Definition (Options.boxed_definitions()))
       | IDENT "SubClass"  -> Class.add_subclass_hook, (Global, SubClass)
       | IDENT "Local"; IDENT "SubClass"  ->
           Class.add_subclass_hook, (Local, SubClass) ] ]