diff options
| author | bgregoir | 2006-12-11 18:46:35 +0000 |
|---|---|---|
| committer | bgregoir | 2006-12-11 18:46:35 +0000 |
| commit | c86d78c0f18fb28f74bb6b192c03ebe73117cf03 (patch) | |
| tree | 99294164215016607e4056e5730a2d6c91043dbf /contrib/interface | |
| parent | 70c88a5f6d7e1ef184d70512969a6221eec8d11e (diff) | |
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
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/ascent.mli | 1 | ||||
| -rw-r--r-- | contrib/interface/vtp.ml | 3 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 1 |
3 files changed, 5 insertions, 0 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index b6cc55f617..ef1d095e20 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -642,6 +642,7 @@ and ct_TACTIC_COM = | CT_elim_type of ct_FORMULA | CT_exact of ct_FORMULA | CT_exact_no_check of ct_FORMULA + | CT_vm_cast_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/vtp.ml b/contrib/interface/vtp.ml index fe227f9958..166a0cbf63 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -1549,6 +1549,9 @@ and fTACTIC_COM = function | CT_exact_no_check(x1) -> fFORMULA x1; fNODE "exact_no_check" 1 +| CT_vm_cast_no_check(x1) -> + fFORMULA x1; + fNODE "vm_cast_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 6c9e8239db..1d710ed3de 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1060,6 +1060,7 @@ and xlate_tac = | TacAssumption -> CT_assumption | TacExact c -> CT_exact (xlate_formula c) | TacExactNoCheck c -> CT_exact_no_check (xlate_formula c) + | TacVmCastNoCheck c -> CT_vm_cast_no_check (xlate_formula c) | TacDestructHyp (true, (_,id)) -> CT_cdhyp (xlate_ident id) | TacDestructHyp (false, (_,id)) -> CT_dhyp (xlate_ident id) | TacDestructConcl -> CT_dconcl |