diff options
Diffstat (limited to 'contrib/interface/vtp.ml')
| -rw-r--r-- | contrib/interface/vtp.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 675b024ce..48047cf96 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -1282,6 +1282,7 @@ and fRED_COM = function fPATTERN_NE_LIST x1; fNODE "pattern" 1 | CT_red -> fNODE "red" 0 +| CT_cbvvm -> fNODE "vm_compute" 0 | CT_simpl(x1) -> fPATTERN_OPT x1; fNODE "simpl" 1 @@ -1546,6 +1547,9 @@ and fTACTIC_COM = function | CT_exact(x1) -> fFORMULA x1; fNODE "exact" 1 +| CT_exact_no_check(x1) -> + fFORMULA x1; + fNODE "exact_no_check" 1 | CT_exists(x1) -> fSPEC_LIST x1; fNODE "exists" 1 |