COMMITED BYTECODE COMPILER

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

3 files changed, 12 insertions, 6 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 35cd2ea2c6..3e08fae301 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -773,6 +773,7 @@ let pr_red_expr (pr_constr,pr_lconstr,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 test prc prlc pr2 = function
   | ConstrEval (r,c) ->
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 7596dc2c33..0dbf05aac9 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -487,6 +487,7 @@ and pr_atom1 env = function
        pr_lident id2)
   | TacAssumption as t -> pr_atom0 env t
   | TacExact c -> hov 1 (str "exact" ++ pr_constrarg env c)
+  | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg env c)
   | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings env cb)
   | TacElim (cb,cbo) ->
       hov 1 (str "elim" ++ pr_arg (pr_with_bindings env) cb ++ 
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 085dcccb10..ecf7b76a19 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -578,8 +578,10 @@ let rec pr_vernac = function
       let pr_def_token = function
         | Local, Coercion -> str"Coercion Local"
         | Global, Coercion -> str"Coercion"
-        | Local, Definition -> str"Let"
-        | Global, Definition -> str"Definition"
+        | Local, Definition _ -> str"Let"
+        | Global, Definition b ->
+	    if b then str"Boxed Definition"
+	    else str"Definition"
         | Local, SubClass -> str"Local SubClass"
         | Global, SubClass -> str"SubClass"
         | Global, CanonicalStructure -> str"Canonical Structure"
@@ -726,7 +728,7 @@ let rec pr_vernac = function
       (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
 
 
-  | VernacFixpoint recs ->
+  | VernacFixpoint (recs,b) ->
 
       (* Copie simplifiée de command.ml pour recalculer les implicites *)
       (* les notations, et le contexte d'evaluation *)
@@ -792,10 +794,11 @@ let rec pr_vernac = function
             ++ str" :=" ++ brk(1,1) ++ ppc ++ 
 	    pr_decl_notation pr_constr ntn
       in
-      hov 1 (str"Fixpoint" ++ spc() ++
+      let start = if b then "Boxed Fixpoint" else "Fixpoint" in
+      hov 1 (str start ++ spc() ++
         prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs)
 
-  | VernacCoFixpoint corecs ->
+  | VernacCoFixpoint (corecs,b) ->
       let pr_onecorec (id,bl,c,def) =
         let (bl',def,c) =
               if Options.do_translate() then extract_def_binders def c
@@ -804,7 +807,8 @@ let rec pr_vernac = function
         pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
         spc() ++ pr_type c ++
         str" :=" ++ brk(1,1) ++ pr_lconstr def in
-      hov 1 (str"CoFixpoint" ++ spc() ++
+      let start = if b then "Boxed CoFixpoint" else "CoFixpoint" in
+      hov 1 (str start ++ spc() ++
       prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs)  
   | VernacScheme l ->
       hov 2 (str"Scheme" ++ spc() ++