Update docgram following #12122 and #12229.

1 files changed, 7 insertions, 54 deletions

diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 92e9df51d5..71d0251339 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -798,58 +798,7 @@ gallina: [
 ]
 
 register_token: [
-| register_prim_token
-| register_type_token
-]
-
-register_type_token: [
-| "#int63_type"
-| "#float64_type"
-]
-
-register_prim_token: [
-| "#int63_head0"
-| "#int63_tail0"
-| "#int63_add"
-| "#int63_sub"
-| "#int63_mul"
-| "#int63_div"
-| "#int63_mod"
-| "#int63_lsr"
-| "#int63_lsl"
-| "#int63_land"
-| "#int63_lor"
-| "#int63_lxor"
-| "#int63_addc"
-| "#int63_subc"
-| "#int63_addcarryc"
-| "#int63_subcarryc"
-| "#int63_mulc"
-| "#int63_diveucl"
-| "#int63_div21"
-| "#int63_addmuldiv"
-| "#int63_eq"
-| "#int63_lt"
-| "#int63_le"
-| "#int63_compare"
-| "#float64_opp"
-| "#float64_abs"
-| "#float64_eq"
-| "#float64_lt"
-| "#float64_le"
-| "#float64_compare"
-| "#float64_classify"
-| "#float64_add"
-| "#float64_sub"
-| "#float64_mul"
-| "#float64_div"
-| "#float64_sqrt"
-| "#float64_of_int63"
-| "#float64_normfr_mantissa"
-| "#float64_frshiftexp"
-| "#float64_ldshiftexp"
-| "#float64_next_up"
-| "#float64_next_down"
+| test_hash_ident "#" IDENT
 ]
 
 thm_token: [
@@ -1910,9 +1859,13 @@ debug: [
 |
 ]
 
+eauto_search_strategy_name: [
+| "bfs"
+| "dfs"
+]
+
 eauto_search_strategy: [
-| "(bfs)"
-| "(dfs)"
+| "(" eauto_search_strategy_name ")"
 |
 ]