COMMITED BYTECODE COMPILER

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

7 files changed, 27 insertions, 14 deletions

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 0f61d3b0e2..a33d648ed2 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -28,6 +28,7 @@ let h_intro x        = h_intro_move (Some x) None
 let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x)
 let h_assumption     = abstract_tactic TacAssumption assumption
 let h_exact c        = abstract_tactic (TacExact c) (exact_check c)
+let h_exact_no_check c = abstract_tactic (TacExactNoCheck c) (exact_no_check c)
 let h_apply cb       = abstract_tactic (TacApply cb) (apply_with_bindings cb)
 let h_elim cb cbo    = abstract_tactic (TacElim (cb,cbo)) (elim cb cbo)
 let h_elim_type c    = abstract_tactic (TacElimType c) (elim_type c)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 711e71d919..ddfb9bd12a 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -29,6 +29,7 @@ val h_intros_until    : quantified_hypothesis -> tactic
 
 val h_assumption      : tactic
 val h_exact           : constr -> tactic
+val h_exact_no_check  : constr -> tactic
 
 val h_apply           : constr with_bindings -> tactic
 
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 9fd54ee694..77d9233d19 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -246,8 +246,9 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
   let _ = 
     declare_constant name
     (DefinitionEntry { const_entry_body = invProof;
-                     const_entry_type = None;
-                     const_entry_opaque = false }, 
+                       const_entry_type = None;
+                       const_entry_opaque = false;
+		       const_entry_boxed = true}, 
      IsProof Lemma)
   in ()
 
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index cf0388543d..a1873770ba 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -690,7 +690,8 @@ let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) =
               [| argsconstr; outputconstr; apply_to_rels m quantifiers_rev ;
                   apply_to_rels mext quantifiers_rev |]));
           const_entry_type = None;
-          const_entry_opaque = false},
+          const_entry_opaque = false;
+          const_entry_boxed = false},
            IsDefinition)) ;
      mext 
  in
@@ -993,7 +994,8 @@ let int_add_relation id a aeq refl sym trans =
             Name (id_of_string "X"),None,mkType (Termops.new_univ ())] @
             a_quantifiers_rev);
        const_entry_type = None;
-       const_entry_opaque = false},
+       const_entry_opaque = false;
+       const_entry_boxed = false},
       IsDefinition) in
   let id_precise = id_of_string (string_of_id id ^ "_precise_relation_class") in
   let xreflexive_relation_class =
@@ -1009,7 +1011,8 @@ let int_add_relation id a aeq refl sym trans =
       {const_entry_body =
         Sign.it_mkLambda_or_LetIn xreflexive_relation_class a_quantifiers_rev;
        const_entry_type = None;
-       const_entry_opaque = false},
+       const_entry_opaque = false;
+       const_entry_boxed = false },
       IsDefinition) in
   let aeq_rel =
    { aeq_rel with
@@ -1068,7 +1071,8 @@ let int_add_relation id a aeq refl sym trans =
         (DefinitionEntry
           {const_entry_body = Sign.it_mkLambda_or_LetIn lemma a_quantifiers_rev;
            const_entry_type = None;
-           const_entry_opaque = false},
+           const_entry_opaque = false;
+          const_entry_boxed = false},
           IsDefinition)
       in
        let a_quantifiers_rev =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 6f459b15ce..00dc193325 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -552,7 +552,7 @@ let intern_redexp ist = function
   | Lazy f -> Lazy (intern_flag ist f)
   | Pattern l -> Pattern (List.map (intern_constr_occurrence ist) l)
   | Simpl o -> Simpl (option_app (intern_constr_occurrence ist) o)
-  | (Red _ | Hnf as r) -> r
+  | (Red _ | Hnf | CbvVm as r ) -> r
   | ExtraRedExpr (s,c) -> ExtraRedExpr (s, intern_constr ist c)
 
 let intern_inversion_strength lf ist = function
@@ -637,6 +637,7 @@ let rec intern_atomic lf ist x =
           option_app (intern_hyp ist) ido')
   | TacAssumption -> TacAssumption
   | TacExact c -> TacExact (intern_constr ist c)
+  | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
   | TacApply cb -> TacApply (intern_constr_with_bindings ist cb)
   | TacElim (cb,cbo) ->
       TacElim (intern_constr_with_bindings ist cb,
@@ -1233,7 +1234,7 @@ let redexp_interp ist sigma env = function
   | Lazy f -> Lazy (interp_flag ist env f)
   | Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l)
   | Simpl o -> Simpl (option_app (interp_pattern ist sigma env) o)
-  | (Red _ |  Hnf as r) -> r
+  | (Red _ |  Hnf | CbvVm as r) -> r
   | ExtraRedExpr (s,c) -> ExtraRedExpr (s,interp_constr ist sigma env c)
 
 let pf_redexp_interp ist gl = redexp_interp ist (project gl) (pf_env gl)
@@ -1653,6 +1654,7 @@ and interp_atomic ist gl = function
       (option_app (interp_hyp ist gl) ido')
   | TacAssumption -> h_assumption
   | TacExact c -> h_exact (pf_interp_casted_constr ist gl c)
+  | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c)
   | TacApply cb -> h_apply (interp_constr_with_bindings ist gl cb)
   | TacElim (cb,cbo) ->
       h_elim (interp_constr_with_bindings ist gl cb)
@@ -1894,7 +1896,7 @@ let subst_redexp subst = function
   | Lazy f -> Lazy (subst_flag subst f)
   | Pattern l -> Pattern (List.map (subst_constr_occurrence subst) l)
   | Simpl o -> Simpl (option_app (subst_constr_occurrence subst) o)
-  | (Red _ | Hnf as r) -> r
+  | (Red _ | Hnf | CbvVm as r) -> r
   | ExtraRedExpr (s,c) -> ExtraRedExpr (s, subst_rawconstr subst c)
 
 let subst_raw_may_eval subst = function
@@ -1918,6 +1920,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacIntroPattern _ | TacIntrosUntil _ | TacIntroMove _ as x -> x
   | TacAssumption as x -> x
   | TacExact c -> TacExact (subst_rawconstr subst c)
+  | TacExactNoCheck c -> TacExactNoCheck (subst_rawconstr subst c)
   | TacApply cb -> TacApply (subst_raw_with_bindings subst cb)
   | TacElim (cb,cbo) ->
       TacElim (subst_raw_with_bindings subst cb,
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 3d91877d00..0a0589e967 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -369,7 +369,7 @@ let general_elim_then_using
     match predicate with
        | None   -> elimclause'
        | Some p ->
-           clenv_unify true Evd.CONV (mkMeta pmv) p elimclause'
+           clenv_unify true Reduction.CONV (mkMeta pmv) p elimclause'
   in 
   elim_res_pf_THEN_i elimclause' branchtacs gl
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ad17f52483..11f2e38fe3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -184,10 +184,12 @@ let change_and_check cv_pb t env sigma c =
 (* Use cumulutavity only if changing the conclusion not a subterm *)
 let change_on_subterm cv_pb t = function
   | None -> change_and_check cv_pb t
-  | Some occl -> contextually false occl (change_and_check CONV t) 
+  | Some occl -> contextually false occl (change_and_check Reduction.CONV t) 
 
-let change_in_concl occl t = reduct_in_concl (change_on_subterm CUMUL t occl) 
-let change_in_hyp occl t   = reduct_in_hyp (change_on_subterm CONV t occl)
+let change_in_concl occl t =
+  reduct_in_concl (change_on_subterm Reduction.CUMUL t occl) 
+let change_in_hyp occl t   =
+  reduct_in_hyp (change_on_subterm Reduction.CONV t occl)
 
 let change_option occl t = function
     Some id -> change_in_hyp occl t id
@@ -1662,7 +1664,8 @@ let elim_scheme_type elim t gl =
     | Meta mv ->
         let clause' =
 	  (* t is inductive, then CUMUL or CONV is irrelevant *)
-	  clenv_unify true CUMUL t (clenv_meta_type clause mv) clause in
+	  clenv_unify true Reduction.CUMUL t
+            (clenv_meta_type clause mv) clause in
 	res_pf clause' ~allow_K:true gl
     | _ -> anomaly "elim_scheme_type"