COMMITED BYTECODE COMPILER

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

7 files changed, 36 insertions, 11 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 7c4fa0d5bc..5ba7d591e5 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -165,6 +165,7 @@ GEXTEND Gram
       | IDENT "Cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s)
       | IDENT "Lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s)
       | IDENT "Compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta])
+      | IDENT "Vm_compute" -> CbvVm
       | IDENT "Unfold"; ul = LIST1 unfold_occ -> Unfold ul
       | IDENT "Fold"; cl = LIST1 constr -> Fold cl
       | IDENT "Pattern"; pl = LIST1 pattern_occ -> Pattern pl ] ]
@@ -180,6 +181,7 @@ GEXTEND Gram
       | IDENT "Unfold"; ul = LIST1 unfold_occ -> Unfold ul
       | IDENT "Fold"; cl = LIST1 constr -> Fold cl
       | IDENT "Pattern"; pl = LIST1 pattern_occ -> Pattern pl
+      | IDENT "Vm_compute" -> CbvVm   
       | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ]
   ;
   hypident:
@@ -250,7 +252,8 @@ GEXTEND Gram
 
       | IDENT "Assumption" -> TacAssumption
       | IDENT "Exact"; c = constr -> TacExact c
-
+      | IDENT "Exact_no_check"; c = constr -> TacExactNoCheck c
+      
       | IDENT "Apply"; cl = constr_with_bindings -> TacApply cl
       | IDENT "Elim"; cl = constr_with_bindings; el = OPT eliminator ->
           TacElim (cl,el)
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 4a62631391..8930c8dcad 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -197,6 +197,7 @@ GEXTEND Gram
       | IDENT "cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s)
       | IDENT "lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s)
       | IDENT "compute" -> compute
+      | IDENT "vm_compute" -> CbvVm
       | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
       | IDENT "pattern"; pl = LIST1 pattern_occ SEP","-> Pattern pl ] ]
@@ -209,6 +210,7 @@ GEXTEND Gram
       | IDENT "cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s)
       | IDENT "lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s)
       | IDENT "compute" -> compute
+      | IDENT "vm_compute" -> CbvVm
       | IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
       | IDENT "pattern"; pl = LIST1 pattern_occ -> Pattern pl
@@ -278,6 +280,7 @@ GEXTEND Gram
 
       | IDENT "assumption" -> TacAssumption
       | IDENT "exact"; c = constr -> TacExact c
+      | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c
 
       | IDENT "apply"; cl = constr_with_bindings -> TacApply cl
       | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator ->
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index fbfd35863e..43e6b81cc1 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -109,8 +109,10 @@ GEXTEND Gram
       | IDENT "Remark" -> Remark ] ]
   ;
   def_token:
-    [ [ "Definition" -> (fun _ _ -> ()), (Global, Definition)
-      | IDENT "Local" -> (fun _ _ -> ()), (Local, Definition)
+    [ [ IDENT "Boxed";"Definition" ->
+	 (fun _ _ -> ()), (Global, Definition true)
+      | "Definition" -> (fun _ _ -> ()), (Global, Definition false)
+      | IDENT "Local" -> (fun _ _ -> ()), (Local, Definition true)
       | IDENT "SubClass"  -> Class.add_subclass_hook, (Global, SubClass)
       | IDENT "Local"; IDENT "SubClass"  ->
 	  Class.add_subclass_hook, (Local, SubClass) ] ] 
@@ -315,8 +317,12 @@ GEXTEND Gram
           VernacInductive (f,indl)
       | f = finite_token; indl = LIST1 oneind SEP "with" ->
           VernacInductive (f,indl)
-      | "Fixpoint"; recs = specifrec -> VernacFixpoint recs
-      | "CoFixpoint"; corecs = specifcorec -> VernacCoFixpoint corecs
+      | IDENT "Boxed"; "Fixpoint"; recs = specifrec ->
+	 VernacFixpoint (recs,true)
+      | "Fixpoint"; recs = specifrec -> VernacFixpoint (recs,false)
+      | IDENT "Boxed"; "CoFixpoint"; corecs = specifcorec -> 
+	 VernacCoFixpoint (corecs,true)
+      | "CoFixpoint"; corecs = specifcorec -> VernacCoFixpoint (corecs,false)
       | 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 def78d92a2..9cf0d3a210 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -96,21 +96,28 @@ GEXTEND Gram
     [ [ thm = thm_token; id = identref; bl = LIST0 binder_let; ":";
         c = lconstr ->
           VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ()))
-      | (f,d) = def_token; id = identref; b = def_body -> 
-          VernacDefinition (d, id, b, f)
       | stre = assumption_token; bl = assum_list -> 
 	  VernacAssumption (stre, bl)
       | stre = assumptions_token; bl = assum_list ->
 	  test_plurial_form bl;
 	  VernacAssumption (stre, bl)
+      | IDENT "Boxed";"Definition";id = identref; b = def_body -> 
+	  VernacDefinition ((Global,Definition true), id, b, (fun _ _ -> ()))
+      | (f,d) = def_token; id = identref; b = def_body -> 
+          VernacDefinition (d, id, b, f)
       (* Gallina inductive declarations *)
       | f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
           VernacInductive (f,indl)
+      | IDENT "Boxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
+          VernacFixpoint (recs,true)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint recs
+          VernacFixpoint (recs,false)
+      | IDENT "Boxed"; "CoFixpoint"; 
+	   corecs = LIST1 corec_definition SEP "with" ->
+          VernacCoFixpoint (corecs,true)
       | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint corecs
+          VernacCoFixpoint (corecs,false)
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ]
   ;
   gallina_ext:
@@ -133,8 +140,8 @@ GEXTEND Gram
       | IDENT "Remark" -> Remark ] ]
   ;
   def_token:
-    [ [ "Definition" -> (fun _ _ -> ()), (Global, Definition)
-      | IDENT "Let" -> (fun _ _ -> ()), (Local, Definition)
+    [ [ "Definition" -> (fun _ _ -> ()), (Global, Definition false)
+      | IDENT "Let" -> (fun _ _ -> ()), (Local, Definition false)
       | IDENT "SubClass"  -> Class.add_subclass_hook, (Global, SubClass)
       | IDENT "Local"; IDENT "SubClass"  ->
           Class.add_subclass_hook, (Local, SubClass) ] ] 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 3a02e5f25f..3bfd26d72b 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -372,6 +372,8 @@ let pr_red_expr (pr_constr,pr_ref) = function
   | Red true -> error "Shouldn't be accessible from user"
   | ExtraRedExpr (s,c) ->
       hov 1 (str s ++ pr_arg pr_constr c)
+  | CbvVm -> str "vm_compute" 
+
 
 let rec pr_may_eval pr pr2 = function
   | ConstrEval (r,c) ->
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 8c78e4fc70..3057e41a41 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -456,6 +456,7 @@ and pr_atom1 = function
       (str "Intro" ++ pr_opt pr_id ido1 ++ spc () ++ str "after " ++ pr_id id2)
   | TacAssumption as t -> pr_atom0 t
   | TacExact c -> hov 1 (str "Exact" ++ pr_arg pr_constr c)
+  | TacExactNoCheck c -> hov 1 (str "Exact_no_check" ++ pr_arg pr_constr c)
   | TacApply cb -> hov 1 (str "Apply" ++ spc () ++ pr_with_bindings cb)
   | TacElim (cb,cbo) ->
       hov 1 (str "Elim" ++ pr_arg pr_with_bindings cb ++ 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 3ed0256ff8..ec1e6410e8 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -248,6 +248,7 @@ let mlexpr_of_red_expr = function
   | Rawterm.Pattern l ->
       let f = mlexpr_of_list mlexpr_of_occ_constr in
       <:expr< Rawterm.Pattern $f l$ >>
+  | Rawterm.CbvVm -> <:expr< Rawterm.CbvVm >>
   | Rawterm.ExtraRedExpr (s,c) ->
       let l = mlexpr_of_constr c in
       <:expr< Rawterm.ExtraRedExpr $mlexpr_of_string s$ $l$ >>
@@ -350,6 +351,8 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacAssumption >>
   | Tacexpr.TacExact c ->
       <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >>
+  | Tacexpr.TacExactNoCheck c ->
+      <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >>
   | Tacexpr.TacApply cb ->
       <:expr< Tacexpr.TacApply $mlexpr_of_constr_with_binding cb$ >>
   | Tacexpr.TacElim (cb,cbo) ->