aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface/vtp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/vtp.ml')
-rw-r--r--contrib/interface/vtp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index f55eee07d5..76b71be425 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -1567,7 +1567,7 @@ and fTACTIC_COM = function
fFORMULA x1 ++
fNODE "exact_no_check" 1
| CT_vm_cast_no_check(x1) ->
- fFORMULA x1;
+ fFORMULA x1 ++
fNODE "vm_cast_no_check" 1
| CT_exists(x1) ->
fSPEC_LIST x1 ++