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


From 86cdd51c4e25fceb12854863419fbdc3f19e44aa Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 16 Nov 2019 11:03:49 +0100
Subject: Stop keeping outdated static list of keywords.

The real list is computed by tok_using in CLexer.
---
 plugins/ltac/g_tactic.mlg | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 6a158bde17..e51b1f051d 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -30,9 +30,6 @@ open Pcoq
 
 let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta]
 
-let tactic_kw = [ "->"; "<-" ; "by" ]
-let _ = List.iter CLexer.add_keyword tactic_kw
-
 let err () = raise Stream.Failure
 
 (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
-- 
cgit v1.2.3


From 20f0e2efb87541e511cf31e220a44e4376c44550 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 2 May 2020 23:22:48 +0200
Subject: Moving lazymatch and multimatch to simple identifiers.

---
 plugins/ltac/g_ltac.mlg | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 5baa23b3e9..0dea4fcc43 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -216,8 +216,8 @@ GRAMMAR EXTEND Gram
   ;
   match_key:
     [ [ "match" -> { Once }
-      | "lazymatch" -> { Select }
-      | "multimatch" -> { General } ] ]
+      | IDENT "lazymatch" -> { Select }
+      | IDENT "multimatch" -> { General } ] ]
   ;
   input_fun:
     [ [ "_" -> { Name.Anonymous }
-- 
cgit v1.2.3