COMMITED BYTECODE COMPILER

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

4 files changed, 16 insertions, 7 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index d246e7323..88ffb2bce 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -531,6 +531,7 @@ and ct_RED_COM =
   | CT_lazy of ct_CONVERSION_FLAG_LIST * ct_CONV_SET
   | CT_pattern of ct_PATTERN_NE_LIST
   | CT_red
+  | CT_cbvvm
   | CT_simpl of ct_PATTERN_OPT
   | CT_unfold of ct_UNFOLD_NE_LIST
 and ct_RETURN_INFO =
@@ -638,6 +639,7 @@ and ct_TACTIC_COM =
   | CT_elim of ct_FORMULA * ct_SPEC_LIST * ct_USING
   | CT_elim_type of ct_FORMULA
   | CT_exact of ct_FORMULA
+  | CT_exact_no_check of ct_FORMULA
   | CT_exists of ct_SPEC_LIST
   | CT_fail of ct_ID_OR_INT * ct_STRING_OPT
   | CT_first of ct_TACTIC_COM * ct_TACTIC_COM list
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index eaff09688..a08f2cd6f 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -160,7 +160,7 @@ let make_variable_ast name typ implicits =
     
 
 let make_definition_ast name c typ implicits =
-  VernacDefinition ((Global,Definition), (dummy_loc,name), DefineBody ([], None,
+  VernacDefinition ((Global,Definition false), (dummy_loc,name), DefineBody ([], None,
     (constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
     (fun _ _ -> ()))
   ::(implicits_to_ast_list implicits);;
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 675b024ce..48047cf96 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -1282,6 +1282,7 @@ and fRED_COM = function
    fPATTERN_NE_LIST x1;
    fNODE "pattern" 1
 | CT_red -> fNODE "red" 0
+| CT_cbvvm -> fNODE "vm_compute" 0
 | CT_simpl(x1) ->
    fPATTERN_OPT x1;
    fNODE "simpl" 1
@@ -1546,6 +1547,9 @@ and fTACTIC_COM = function
 | CT_exact(x1) ->
    fFORMULA x1;
    fNODE "exact" 1
+| CT_exact_no_check(x1) ->
+   fFORMULA x1;
+   fNODE "exact_no_check" 1
 | CT_exists(x1) ->
    fSPEC_LIST x1;
    fNODE "exists" 1
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index c7ab08526..a997e3095 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -725,6 +725,7 @@ and xlate_red_tactic =
  function
   | Red true -> xlate_error ""
   | Red false -> CT_red
+  | CbvVm -> CT_cbvvm
   | Hnf -> CT_hnf
   | Simpl None -> CT_simpl ctv_PATTERN_OPT_NONE
   | Simpl (Some (l,c)) -> 
@@ -1018,6 +1019,7 @@ and xlate_tac =
     | TacTransitivity c -> CT_transitivity (xlate_formula c)
     | TacAssumption -> CT_assumption
     | TacExact c -> CT_exact (xlate_formula c)
+    | TacExactNoCheck c -> CT_exact_no_check (xlate_formula c)
     | TacDestructHyp (true, (_,id)) -> CT_cdhyp (xlate_ident id)
     | TacDestructHyp (false, (_,id)) -> CT_dhyp (xlate_ident id)
     | TacDestructConcl -> CT_dconcl
@@ -1345,8 +1347,9 @@ let xlate_thm x = CT_thm (match x with
 
 
 let xlate_defn x = CT_defn (match x with
- | (Local, Definition) -> "Local"
- | (Global, Definition) -> "Definition"
+ | (Local, Definition _) -> "Local"
+ | (Global, Definition true) -> "Boxed Definition"
+ | (Global, Definition false) -> "Definition"
  | (Global, SubClass) -> "SubClass"
  | (Global, Coercion) -> "Coercion"
  | (Local, SubClass) -> "Local SubClass"
@@ -1858,8 +1861,8 @@ let rec xlate_vernac =
 	     translate_opt_notation_decl notopt) in
         CT_mind_decl
 	  (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi))
-   | VernacFixpoint [] -> xlate_error "mutual recursive"
-   | VernacFixpoint (lm :: lmi) ->
+   | VernacFixpoint ([],_) -> xlate_error "mutual recursive"
+   | VernacFixpoint ((lm :: lmi),boxed) ->
       let strip_mutrec ((fid, n, bl, arf, ardef), ntn) =
         let (struct_arg,bl,arf,ardef) =
          if bl = [] then
@@ -1876,8 +1879,8 @@ let rec xlate_vernac =
           | _ -> xlate_error "mutual recursive" in
         CT_fix_decl
 	  (CT_fix_rec_list (strip_mutrec lm, List.map strip_mutrec lmi))
-   | VernacCoFixpoint [] -> xlate_error "mutual corecursive"
-   | VernacCoFixpoint (lm :: lmi) ->
+   | VernacCoFixpoint ([],boxed) -> xlate_error "mutual corecursive"
+   | VernacCoFixpoint ((lm :: lmi),boxed) ->
       let strip_mutcorec (fid, bl, arf, ardef) =
 	CT_cofix_rec (xlate_ident fid, xlate_binder_list bl,
                       xlate_formula arf, xlate_formula ardef) in