diff options
Diffstat (limited to 'contrib/interface/ascent.mli')
| -rw-r--r-- | contrib/interface/ascent.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index 2eb2c38126..c2035586fb 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -164,7 +164,7 @@ and ct_COMMAND = | CT_resume of ct_ID_OPT | CT_save of ct_THM_OPT * ct_ID_OPT | CT_scomments of ct_SCOMMENT_CONTENT_LIST - | CT_search of ct_ID * ct_IN_OR_OUT_MODULES + | CT_search of ct_FORMULA * ct_IN_OR_OUT_MODULES | CT_search_about of ct_ID_OR_STRING_NE_LIST * ct_IN_OR_OUT_MODULES | CT_search_pattern of ct_FORMULA * ct_IN_OR_OUT_MODULES | CT_search_rewrite of ct_FORMULA * ct_IN_OR_OUT_MODULES |