diff options
| author | Jim Fehrle | 2020-04-01 13:18:03 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-06-08 16:50:53 -0700 |
| commit | 27d6686f399f40904ff6005a84677907d53c5bbf (patch) | |
| tree | 5a27b8acdab8ce79b9a7d10685c8979cda82416b /doc/tools/docgram/fullGrammar | |
| parent | 6a76e4394876cb08b02d8e7ea185049147f9cd2b (diff) | |
Convert Ltac chapter to prodn
Diffstat (limited to 'doc/tools/docgram/fullGrammar')
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 1b0a5c28ee..c5edb538b7 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1425,7 +1425,7 @@ simple_tactic: [ | "firstorder" OPT tactic firstorder_using "with" LIST1 preident | "gintuition" OPT tactic | "functional" "inversion" quantified_hypothesis OPT reference (* funind plugin *) -| "functional" "induction" LIST1 constr fun_ind_using with_names (* funind plugin *) +| "functional" "induction" lconstr fun_ind_using with_names (* funind plugin *) | "soft" "functional" "induction" LIST1 constr fun_ind_using with_names (* funind plugin *) | "reflexivity" | "exact" casted_constr @@ -1591,7 +1591,6 @@ simple_tactic: [ | "auto" OPT int_or_var auto_using hintbases | "info_auto" OPT int_or_var auto_using hintbases | "debug" "auto" OPT int_or_var auto_using hintbases -| "prolog" "[" LIST0 uconstr "]" int_or_var | "eauto" OPT int_or_var OPT int_or_var auto_using hintbases | "new" "auto" OPT int_or_var auto_using hintbases | "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases |