diff options
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 |