From 51ddbbe05ab2c47a2c50c1e6781b8562b7717110 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 14 Nov 2020 10:20:30 -0800
Subject: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"

---
 doc/tools/docgram/fullGrammar | 1 +
 1 file changed, 1 insertion(+)

(limited to 'doc/tools/docgram/fullGrammar')

diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index a787d769fb..033ece04de 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1623,6 +1623,7 @@ simple_tactic: [
 | "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases
 | "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases
 | "dfs" "eauto" OPT int_or_var auto_using hintbases
+| "bfs" "eauto" OPT int_or_var auto_using hintbases
 | "autounfold" hintbases clause_dft_concl
 | "autounfold_one" hintbases "in" hyp
 | "autounfold_one" hintbases
-- 
cgit v1.2.3