Changement dans le kernel :

   - essai de suppression des dependances debiles. (echec) 
   - Application des patch debian.

Pour ring et field :
   - introduciton de la function de sign et de puissance.
   - Correction de certains bug.
   - supression de ring_replace ....

Pour exact_no_check :
   - ajout de la tactic : vm_cast_no_check (t)
     qui remplace "exact_no_check (t<: type of Goal)"
      (cette version forcais l'evaluation du cast dans le 
       pretypage).




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

5 files changed, 12 insertions, 0 deletions

diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 02792cb331..a940b5a0de 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -29,6 +29,8 @@ 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_vm_cast_no_check c = 
+  abstract_tactic (TacVmCastNoCheck c) (vm_cast_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 2823a53ad5..bb1e4f4234 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -30,6 +30,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_vm_cast_no_check  : constr -> tactic
 
 val h_apply           : constr with_bindings -> tactic
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ee70c326f1..8eff3ccd98 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -626,6 +626,7 @@ let rec intern_atomic lf ist x =
   | TacAssumption -> TacAssumption
   | TacExact c -> TacExact (intern_constr ist c)
   | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c)
+  | TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c)
   | TacApply cb -> TacApply (intern_constr_with_bindings ist cb)
   | TacElim (cb,cbo) ->
       TacElim (intern_constr_with_bindings ist cb,
@@ -1992,6 +1993,7 @@ and interp_atomic ist gl = function
   | 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)
+  | TacVmCastNoCheck c -> h_vm_cast_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)
@@ -2320,6 +2322,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacAssumption as x -> x
   | TacExact c -> TacExact (subst_rawconstr subst c)
   | TacExactNoCheck c -> TacExactNoCheck (subst_rawconstr subst c)
+  | TacVmCastNoCheck c -> TacVmCastNoCheck (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/tactics.ml b/tactics/tactics.ml
index f27d116e4a..eba3fa4e43 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -629,6 +629,11 @@ let exact_check c gl =
 
 let exact_no_check = refine_no_check
 
+let vm_cast_no_check c gl = 
+  let concl = pf_concl gl in
+  refine_no_check (Term.mkCast(c,Term.VMcast,concl)) gl
+
+
 let exact_proof c gl =
   (* on experimente la synthese d'ise dans exact *)
   let c = Constrintern.interp_casted_constr (project gl) (pf_env gl) c (pf_concl gl)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c1b8782b3a..ac51f736c1 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -106,6 +106,7 @@ val intros_pattern    : identifier option -> intro_pattern_expr list -> tactic
 
 val assumption       : tactic
 val exact_no_check   : constr -> tactic
+val vm_cast_no_check : constr -> tactic
 val exact_check      : constr -> tactic
 val exact_proof      : Topconstr.constr_expr -> tactic