diff options
| author | Théo Zimmermann | 2021-01-28 21:22:44 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2021-01-28 21:22:44 +0100 |
| commit | f7d37e69a3df1e049e0bee5d3a58ef2e7cf87af9 (patch) | |
| tree | eac7c7d3f6a125290ea41a2cbd8e93445933a379 /doc/tools/docgram/common.edit_mlg | |
| parent | a54a5b83becd3ef7feef1352b56d10a3d74be85f (diff) | |
Replace : term with : type in open binders.
And update the doc_grammar files.
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 "." |