diff options
Diffstat (limited to 'contrib/interface/vtp.ml')
| -rw-r--r-- | contrib/interface/vtp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 946090099..b9daf6357 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -530,7 +530,7 @@ and fCOMMAND = function fSCOMMENT_CONTENT_LIST x1 ++ fNODE "scomments" 1 | CT_search(x1, x2) -> - fID x1 ++ + fFORMULA x1 ++ fIN_OR_OUT_MODULES x2 ++ fNODE "search" 2 | CT_search_about(x1, x2) -> |