From 62f6fb862ce4f3eec46200d11e503aa5d6d051db Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Nov 2019 17:18:06 +0100
Subject: Documenting plugin/tactic/stdlib keywords in corresponding chapters.

Incidentally removing "discriminated", "(bfs)" and "(dfs)" from
keywords. It is enough to make them normal identifiers.

Note:
- keywords reserved by the tactics are: ** [= _eqn |- by using
- keywords reserved by ltac are: lazymatch multimatch ||
---
 plugins/ltac/g_class.mlg | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 0f0341f123..81e745b714 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -54,16 +54,23 @@ END
 
 {
 
+let pr_search_strategy_name _prc _prlc _prt = function
+  | Dfs -> Pp.str "dfs"
+  | Bfs -> Pp.str "bfs"
+
 let pr_search_strategy _prc _prlc _prt = function
-  | Some Dfs -> Pp.str "dfs"
-  | Some Bfs -> Pp.str "bfs"
+  | Some s -> pr_search_strategy_name _prc _prlc _prt s
   | None -> Pp.mt ()
 
 }
 
+ARGUMENT EXTEND eauto_search_strategy_name PRINTED BY { pr_search_strategy_name }
+| [ "bfs" ] -> { Bfs }
+| [ "dfs" ] -> { Dfs }
+END
+
 ARGUMENT EXTEND eauto_search_strategy PRINTED BY { pr_search_strategy }
-| [ "(bfs)" ] -> { Some Bfs }
-| [ "(dfs)" ] -> { Some Dfs }
+| [ "(" eauto_search_strategy_name(s) ")" ] -> { Some s }
 | [ ] -> { None }
 END
 
-- 
cgit v1.2.3