From f7d37e69a3df1e049e0bee5d3a58ef2e7cf87af9 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 28 Jan 2021 21:22:44 +0100
Subject: Replace : term with : type in open binders.

And update the doc_grammar files.
---
 doc/tools/docgram/common.edit_mlg | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'doc/tools/docgram/common.edit_mlg')

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 "."
-- 
cgit v1.2.3