From c86d78c0f18fb28f74bb6b192c03ebe73117cf03 Mon Sep 17 00:00:00 2001 From: bgregoir Date: Mon, 11 Dec 2006 18:46:35 +0000 Subject: 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 --- tactics/hiddentac.ml | 2 ++ tactics/hiddentac.mli | 1 + tactics/tacinterp.ml | 3 +++ tactics/tactics.ml | 5 +++++ tactics/tactics.mli | 1 + 5 files changed, 12 insertions(+) (limited to 'tactics') 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 -- cgit v1.2.3