Replace : term with : type in open binders.

And update the doc_grammar files.

4 files changed, 3 insertions, 36 deletions

diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst
index 8dbc1626ba..7566996ef6 100644
--- a/doc/sphinx/language/core/assumptions.rst
+++ b/doc/sphinx/language/core/assumptions.rst
@@ -9,7 +9,7 @@ Binders
 .. insertprodn open_binders binder
 
 .. prodn::
-   open_binders ::= {+ @name } : @term
+   open_binders ::= {+ @name } : @type
    | {+ @binder }
    name ::= _
    | @ident
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 "."
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index ec23ffe83e..bc6b803bbb 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -687,17 +687,6 @@ command: [
 | "Add" "Zify" "BinOpSpec" constr      (* micromega plugin *)
 | "Add" "Zify" "UnOpSpec" constr      (* micromega plugin *)
 | "Add" "Zify" "Saturate" constr      (* micromega plugin *)
-| "Add" "InjTyp" constr      (* micromega plugin *)
-| "Add" "BinOp" constr      (* micromega plugin *)
-| "Add" "UnOp" constr      (* micromega plugin *)
-| "Add" "CstOp" constr      (* micromega plugin *)
-| "Add" "BinRel" constr      (* micromega plugin *)
-| "Add" "PropOp" constr      (* micromega plugin *)
-| "Add" "PropBinOp" constr      (* micromega plugin *)
-| "Add" "PropUOp" constr      (* micromega plugin *)
-| "Add" "BinOpSpec" constr      (* micromega plugin *)
-| "Add" "UnOpSpec" constr      (* micromega plugin *)
-| "Add" "Saturate" constr      (* micromega plugin *)
 | "Show" "Zify" "InjTyp"      (* micromega plugin *)
 | "Show" "Zify" "BinOp"      (* micromega plugin *)
 | "Show" "Zify" "UnOp"      (* micromega plugin *)
@@ -705,7 +694,6 @@ command: [
 | "Show" "Zify" "BinRel"      (* micromega plugin *)
 | "Show" "Zify" "UnOpSpec"      (* micromega plugin *)
 | "Show" "Zify" "BinOpSpec"      (* micromega plugin *)
-| "Show" "Zify" "Spec"      (* micromega plugin *)
 | "Add" "Ring" ident ":" constr OPT ring_mods      (* ring plugin *)
 | "Print" "Rings"      (* ring plugin *)
 | "Add" "Field" ident ":" constr OPT field_mods      (* ring plugin *)
@@ -1258,7 +1246,6 @@ query_command: [
 | "Compute" lconstr "."
 | "Check" lconstr "."
 | "About" smart_global OPT univ_name_list "."
-| "SearchHead" constr_pattern in_or_out_modules "."
 | "SearchPattern" constr_pattern in_or_out_modules "."
 | "SearchRewrite" constr_pattern in_or_out_modules "."
 | "Search" search_query search_queries "."
@@ -1551,7 +1538,6 @@ simple_tactic: [
 | "revert" LIST1 hyp
 | "simple" "induction" quantified_hypothesis
 | "simple" "destruct" quantified_hypothesis
-| "double" "induction" quantified_hypothesis quantified_hypothesis
 | "admit"
 | "fix" ident natural
 | "cofix" ident
@@ -1669,7 +1655,6 @@ simple_tactic: [
 | "autounfold_one" hintbases
 | "unify" constr constr
 | "unify" constr constr "with" preident
-| "convert_concl_no_check" constr
 | "typeclasses" "eauto" "bfs" OPT nat_or_var "with" LIST1 preident
 | "typeclasses" "eauto" OPT nat_or_var "with" LIST1 preident
 | "typeclasses" "eauto" "bfs" OPT nat_or_var
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 75b32a5800..a34e96ac16 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -493,7 +493,7 @@ term_forall_or_fun: [
 ]
 
 open_binders: [
-| LIST1 name ":" term
+| LIST1 name ":" type
 | LIST1 binder
 ]
 
@@ -1001,18 +1001,6 @@ command: [
 | "Reset" "Ltac" "Profile"
 | "Show" "Ltac" "Profile" OPT [ "CutOff" integer | string ]
 | "Show" "Lia" "Profile"      (* micromega plugin *)
-| "Add" "InjTyp" one_term      (* micromega plugin *)
-| "Add" "BinOp" one_term      (* micromega plugin *)
-| "Add" "UnOp" one_term      (* micromega plugin *)
-| "Add" "CstOp" one_term      (* micromega plugin *)
-| "Add" "BinRel" one_term      (* micromega plugin *)
-| "Add" "PropOp" one_term      (* micromega plugin *)
-| "Add" "PropBinOp" one_term      (* micromega plugin *)
-| "Add" "PropUOp" one_term      (* micromega plugin *)
-| "Add" "BinOpSpec" one_term      (* micromega plugin *)
-| "Add" "UnOpSpec" one_term      (* micromega plugin *)
-| "Add" "Saturate" one_term      (* micromega plugin *)
-| "Show" "Zify" "Spec"      (* micromega plugin *)
 | "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" )      (* ring plugin *)
 | "Print" "Rings"      (* ring plugin *)
 | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" )      (* ring plugin *)
@@ -1117,7 +1105,6 @@ command: [
 | "Compute" term
 | "Check" term
 | "About" reference OPT univ_name_list
-| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
@@ -1626,7 +1613,6 @@ simple_tactic: [
 | "revert" LIST1 ident
 | "simple" "induction" [ ident | natural ]
 | "simple" "destruct" [ ident | natural ]
-| "double" "induction" [ ident | natural ] [ ident | natural ]
 | "admit"
 | "clear" LIST0 ident
 | "clear" "-" LIST1 ident
@@ -1758,7 +1744,6 @@ simple_tactic: [
 | "autounfold" OPT hintbases OPT occurrences
 | "autounfold_one" OPT hintbases OPT ( "in" ident )
 | "unify" one_term one_term OPT ( "with" ident )
-| "convert_concl_no_check" one_term
 | "typeclasses" "eauto" OPT "bfs" OPT nat_or_var OPT ( "with" LIST1 ident )
 | "head_of_constr" ident one_term
 | "not_evar" one_term
@@ -2420,7 +2405,6 @@ tac2mode: [
 | "Compute" term
 | "Check" term
 | "About" reference OPT univ_name_list
-| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
 | "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )