diff options
| author | coqbot-app[bot] | 2021-01-28 21:25:59 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-28 21:25:59 +0000 |
| commit | 4ae11ea2bf09fcdf44b1226a45761a2aed34a445 (patch) | |
| tree | f75555ca01275dc1b5331dda71247a04ad141499 /doc/tools/docgram/common.edit_mlg | |
| parent | ed29e0913742c307175846557ed8390a8da771e3 (diff) | |
| parent | f7d37e69a3df1e049e0bee5d3a58ef2e7cf87af9 (diff) | |
Merge PR #13799: Replace : term with : type in open binders.
Reviewed-by: jfehrle
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 8aeb2e564d..27144fd1ad 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -447,7 +447,7 @@ binder: [ open_binders: [ | REPLACE name LIST0 name ":" lconstr -| WITH LIST1 name ":" lconstr +| WITH LIST1 name ":" type (* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *) | DELETE name ".." name | REPLACE name LIST0 name binders @@ -1510,8 +1510,6 @@ query_command: [ | WITH "Check" lconstr | REPLACE "About" smart_global OPT univ_name_list "." | WITH "About" smart_global OPT univ_name_list -| REPLACE "SearchHead" constr_pattern in_or_out_modules "." -| WITH "SearchHead" constr_pattern in_or_out_modules | REPLACE "SearchPattern" constr_pattern in_or_out_modules "." | WITH "SearchPattern" constr_pattern in_or_out_modules | REPLACE "SearchRewrite" constr_pattern in_or_out_modules "." |