Comments (4)
cpitclaudel
commented on June 30, 2024
Is it intended?
No, not sure why they don't happen?
from company-coq.
Matafou
commented on June 30, 2024
Instead there are grammar queries. Maybe the two mechanisms interact badly?
from company-coq.
cpitclaudel
commented on June 30, 2024
I see this:
Welcome to Coq 8.12.2 (January 2021)
<prompt>Coq < 1 || 0 < </prompt>Redirect "/tmp/coqdrloVu" Test Search Output Name Only.
<prompt>Coq < 2 || 0 < </prompt>Timeout 1 Print Grammar tactic.
Entry tactic:tactic_expr is
[ "5" RIGHTA
[ tactic:binder_tactic ]
| "4" LEFTA
[ SELF; ";"; tactic:binder_tactic
| SELF; ";"; SELF
| SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ]
| "3" RIGHTA
[ IDENT "try"; SELF
| IDENT "do"; tactic:int_or_var; SELF
| IDENT "timeout"; tactic:int_or_var; SELF
| IDENT "time"; OPT prim:string; SELF
| IDENT "repeat"; SELF
| IDENT "progress"; SELF
| IDENT "once"; SELF
| IDENT "exactly_once"; SELF
| IDENT "infoH"; SELF
| IDENT "abstract"; NEXT; "using"; constr:ident
| IDENT "abstract"; NEXT
| selector; SELF ]
| "2" RIGHTA
[ SELF; "+"; tactic:binder_tactic
| SELF; "+"; SELF
| SELF; "||"; tactic:binder_tactic
| SELF; "||"; SELF
| IDENT "tryif"; SELF; "then"; SELF; "else"; SELF ]
| "1" RIGHTA
[ IDENT "first"; "["; LIST0 tactic:tactic_expr SEP "|"; "]"
| IDENT "solve"; "["; LIST0 tactic:tactic_expr SEP "|"; "]"
| IDENT "idtac"; LIST0 message_token
| match_key; IDENT "goal"; "with"; match_context_list; "end"
| match_key; IDENT "reverse"; IDENT "goal"; "with"; match_context_list;
"end"
| match_key; SELF; "with"; match_list; "end"
| failkw; [ tactic:int_or_var | ]; LIST0 message_token
| tactic:simple_tactic
| tactic:tactic_arg
| prim:reference; LIST0 tactic_arg_compat ]
| "0" LEFTA
[ "("; SELF; ")"
| "["; ">"; tactic_then_gen; "]"
| tactic_atom ] ]
Entry tactic:binder_tactic is
[ RIGHTA
[ "fun"; LIST1 input_fun; "=>"; tactic:tactic_expr LEVEL "5"
| "let"; [ IDENT "rec" | ]; LIST1 let_clause SEP "with"; "in";
tactic:tactic_expr LEVEL "5"
| IDENT "info"; tactic:tactic_expr LEVEL "5" ] ]
Entry tactic:simple_tactic is
[ LEFTA
[ IDENT "gintuition"; OPT tactic:tactic
| IDENT "firstorder"; OPT tactic:tactic; "with"; LIST1 prim:preident
| IDENT "firstorder"; OPT tactic:tactic; tactic:firstorder_using; "with";
LIST1 prim:preident
| IDENT "firstorder"; OPT tactic:tactic; tactic:firstorder_using
| IDENT "congruence"; "with"; LIST1 constr:constr
| IDENT "congruence"; prim:integer; "with"; LIST1 constr:constr
| IDENT "congruence"; prim:integer
| IDENT "congruence"
| IDENT "dintuition"; tactic:tactic
| IDENT "dintuition"
| IDENT "intuition"; tactic:tactic
| IDENT "intuition"
| IDENT "assert_fails"; tactic:tactic_expr LEVEL "3"
| IDENT "assert_succeeds"; tactic:tactic_expr LEVEL "3"
| IDENT "now"; tactic:tactic
| IDENT "rewrite_all"; "<-"; constr:constr
| IDENT "rewrite_all"; constr:constr
| IDENT "destruct_with_eqn"; ":"; prim:ident; prim:ident
| IDENT "destruct_with_eqn"; ":"; prim:ident; constr:constr
| IDENT "destruct_with_eqn"; prim:ident
| IDENT "destruct_with_eqn"; constr:constr
| IDENT "decide"; IDENT "equality"
| IDENT "decide"; constr:constr; "with"; constr:constr
| IDENT "setoid_transitivity"; constr:constr
| IDENT "setoid_etransitivity"
| IDENT "setoid_symmetry"; "in"; prim:var
| IDENT "setoid_symmetry"
| IDENT "setoid_rewrite"; tactic:orient; tactic:constr_with_bindings; "at";
tactic:occurrences; "in"; prim:var
| IDENT "setoid_rewrite"; tactic:orient; tactic:constr_with_bindings; "at";
tactic:occurrences
| IDENT "setoid_rewrite"; tactic:orient; tactic:constr_with_bindings; "in";
prim:var; "at"; tactic:occurrences
| IDENT "setoid_rewrite"; tactic:orient; tactic:constr_with_bindings; "in";
prim:var
| IDENT "setoid_rewrite"; tactic:orient; tactic:constr_with_bindings
| IDENT "substitute"; tactic:orient; tactic:constr_with_bindings
| IDENT "rewrite_strat"; tactic:rewstrategy; "in"; prim:var
| IDENT "rewrite_strat"; tactic:rewstrategy
| IDENT "rewrite_db"; prim:preident; "in"; prim:var
| IDENT "rewrite_db"; prim:preident
| IDENT "progress_evars"; tactic:tactic
| IDENT "autoapply"; constr:constr; "using"; prim:preident
| IDENT "autoapply"; constr:constr; "with"; prim:preident
| IDENT "head_of_constr"; prim:ident; constr:constr
| IDENT "typeclasses"; IDENT "eauto"; IDENT "bfs"; OPT tactic:int_or_var;
"with"; LIST1 prim:preident
| IDENT "typeclasses"; IDENT "eauto"; OPT tactic:int_or_var; "with";
LIST1 prim:preident
| IDENT "typeclasses"; IDENT "eauto"; OPT tactic:int_or_var
| IDENT "unify"; constr:constr; constr:constr; "with"; prim:preident
| IDENT "unify"; constr:constr; constr:constr
| IDENT "autounfold_one"; tactic:hintbases; "in"; prim:var
| IDENT "autounfold_one"; tactic:hintbases
| IDENT "autounfold"; tactic:hintbases; tactic:clause
| IDENT "dfs"; IDENT "eauto"; OPT tactic:int_or_var; tactic:auto_using;
tactic:hintbases
| IDENT "info_eauto"; OPT tactic:int_or_var; OPT tactic:int_or_var;
tactic:auto_using; tactic:hintbases
| IDENT "new"; IDENT "auto"; OPT tactic:int_or_var; tactic:auto_using;
tactic:hintbases
| IDENT "eauto"; OPT tactic:int_or_var; OPT tactic:int_or_var;
tactic:auto_using; tactic:hintbases
| IDENT "prolog"; "["; LIST0 tactic:uconstr; "]"; tactic:int_or_var
| IDENT "info_auto"; OPT tactic:int_or_var; tactic:auto_using;
tactic:hintbases
| IDENT "auto"; OPT tactic:int_or_var; tactic:auto_using; tactic:hintbases
| IDENT "debug"; IDENT "eauto"; OPT tactic:int_or_var;
OPT tactic:int_or_var; tactic:auto_using; tactic:hintbases
| IDENT "debug"; IDENT "auto"; OPT tactic:int_or_var; tactic:auto_using;
tactic:hintbases
| IDENT "debug"; IDENT "trivial"; tactic:auto_using; tactic:hintbases
| IDENT "info_trivial"; tactic:auto_using; tactic:hintbases
| IDENT "trivial"; tactic:auto_using; tactic:hintbases
| IDENT "finish_timing"; "("; prim:string; ")"; OPT prim:string
| IDENT "finish_timing"; OPT prim:string
| IDENT "restart_timer"; OPT prim:string
| IDENT "show"; IDENT "ltac"; IDENT "profile"; IDENT "cutoff"; prim:integer
| IDENT "show"; IDENT "ltac"; IDENT "profile"; prim:string
| IDENT "show"; IDENT "ltac"; IDENT "profile"
| IDENT "reset"; IDENT "ltac"; IDENT "profile"
| IDENT "stop"; IDENT "ltac"; IDENT "profiling"
| IDENT "start"; IDENT "ltac"; IDENT "profiling"
| IDENT "with_strategy"; tactic:strategy_level_or_var; "[";
LIST1 smart_global; "]"; tactic:tactic_expr LEVEL "3"
| IDENT "guard"; tactic:test
| IDENT "swap"; tactic:int_or_var; tactic:int_or_var
| IDENT "cycle"; tactic:int_or_var
| IDENT "unshelve"; tactic:tactic_expr LEVEL "1"
| IDENT "transparent_abstract"; tactic:tactic_expr LEVEL "3"; "using";
prim:ident
| IDENT "transparent_abstract"; tactic:tactic_expr LEVEL "3"
| IDENT "destauto"; "in"; prim:var
| IDENT "destauto"
| IDENT "hget_evar"; tactic:int_or_var
| IDENT "hresolve_core"; "("; prim:ident; ":="; constr:constr; ")"; "at";
tactic:int_or_var; "in"; constr:constr
| IDENT "hresolve_core"; "("; prim:ident; ":="; constr:constr; ")"; "in";
constr:constr
| IDENT "specialize_eqs"; prim:var
| IDENT "generalize_eqs_vars"; prim:var
| IDENT "generalize_eqs"; prim:var
| IDENT "stepr"; constr:constr; "by"; tactic:tactic
| IDENT "stepr"; constr:constr
| IDENT "stepl"; constr:constr; "by"; tactic:tactic
| IDENT "stepl"; constr:constr
| IDENT "instantiate"; "("; prim:ident; ":="; constr:lconstr; ")"
| IDENT "instantiate"; "("; prim:integer; ":="; constr:lconstr; ")";
tactic:hloc
| IDENT "instantiate"
| IDENT "evar"; tactic:test_lpar_id_colon; "("; prim:ident; ":";
constr:lconstr; ")"
| IDENT "evar"; constr:constr
| IDENT "subst"; LIST1 prim:var
| IDENT "subst"
| IDENT "notypeclasses"; IDENT "refine"; tactic:uconstr
| IDENT "refine"; tactic:uconstr
| IDENT "autorewrite"; "*"; "with"; LIST1 prim:preident; tactic:clause;
"using"; tactic:tactic
| IDENT "autorewrite"; "*"; "with"; LIST1 prim:preident; tactic:clause
| IDENT "autorewrite"; "with"; LIST1 prim:preident; tactic:clause; "using";
tactic:tactic
| IDENT "autorewrite"; "with"; LIST1 prim:preident; tactic:clause
| IDENT "contradiction"; OPT tactic:constr_with_bindings
| IDENT "decompose"; "["; LIST1 constr:constr; "]"; constr:constr
| IDENT "decompose"; IDENT "record"; constr:constr
| IDENT "decompose"; IDENT "sum"; constr:constr
| IDENT "cutrewrite"; tactic:orient; constr:constr; "in"; prim:var
| IDENT "cutrewrite"; tactic:orient; constr:constr
| IDENT "einjection"; "as"; LIST0 tactic:simple_intropattern
| IDENT "einjection"; tactic:destruction_arg; "as";
LIST0 tactic:simple_intropattern
| IDENT "einjection"; tactic:destruction_arg
| IDENT "einjection"
| IDENT "injection"; "as"; LIST0 tactic:simple_intropattern
| IDENT "injection"; tactic:destruction_arg; "as";
LIST0 tactic:simple_intropattern
| IDENT "injection"; tactic:destruction_arg
| IDENT "injection"
| IDENT "ediscriminate"; tactic:destruction_arg
| IDENT "ediscriminate"
| IDENT "discriminate"; tactic:destruction_arg
| IDENT "discriminate"
| IDENT "esimplify_eq"; tactic:destruction_arg
| IDENT "esimplify_eq"
| IDENT "simplify_eq"; tactic:destruction_arg
| IDENT "simplify_eq"
| IDENT "replace"; "<-"; tactic:uconstr; tactic:clause
| IDENT "replace"; "->"; tactic:uconstr; tactic:clause
| IDENT "replace"; tactic:uconstr; "with"; constr:constr; tactic:clause;
tactic:by_arg_tac
| IDENT "replace"; tactic:uconstr; tactic:clause
| IDENT "clearbody"; LIST1 prim:var
| IDENT "clear"; IDENT "dependent"; prim:var
| IDENT "clear"; "-"; LIST1 prim:var
| IDENT "clear"; LIST0 prim:var
| IDENT "double"; IDENT "induction"; tactic:quantified_hypothesis;
tactic:quantified_hypothesis
| IDENT "revert"; IDENT "dependent"; prim:var
| IDENT "revert"; LIST1 prim:var
| IDENT "rename"; LIST1 tactic:rename SEP ","
| IDENT "move"; prim:var; "at"; IDENT "top"
| IDENT "move"; prim:var; "at"; IDENT "bottom"
| IDENT "move"; prim:var; IDENT "after"; prim:var
| IDENT "move"; prim:var; IDENT "before"; prim:var
| IDENT "intro"; "at"; IDENT "top"
| IDENT "intro"; "at"; IDENT "bottom"
| IDENT "intro"; IDENT "after"; prim:var
| IDENT "intro"; IDENT "before"; prim:var
| IDENT "intro"; prim:ident; "at"; IDENT "top"
| IDENT "intro"; prim:ident; "at"; IDENT "bottom"
| IDENT "intro"; prim:ident; IDENT "after"; prim:var
| IDENT "intro"; prim:ident; IDENT "before"; prim:var
| IDENT "intro"; prim:ident
| IDENT "intro"
| IDENT "eexists"; LIST1 tactic:bindings SEP ","
| IDENT "eexists"
| "exists"; LIST1 tactic:bindings SEP ","
| "exists"
| IDENT "esplit"; "with"; tactic:bindings
| IDENT "split"; "with"; tactic:bindings
| IDENT "symmetry"; "in"; tactic:in_clause
| IDENT "specialize"; tactic:constr_with_bindings; "as";
tactic:simple_intropattern
| IDENT "specialize"; tactic:constr_with_bindings
| IDENT "econstructor"; tactic:int_or_var; "with"; tactic:bindings
| IDENT "econstructor"; tactic:int_or_var
| IDENT "econstructor"
| IDENT "constructor"; tactic:int_or_var; "with"; tactic:bindings
| IDENT "constructor"; tactic:int_or_var
| IDENT "constructor"
| IDENT "eright"; "with"; tactic:bindings
| IDENT "right"; "with"; tactic:bindings
| IDENT "eleft"; "with"; tactic:bindings
| IDENT "left"; "with"; tactic:bindings
| IDENT "exact"; constr:constr
| IDENT "intros"; IDENT "until"; tactic:quantified_hypothesis
| IDENT "intros"; ne_intropatterns
| IDENT "intros"
| IDENT "eintros"; ne_intropatterns
| IDENT "eintros"
| IDENT "apply"; "<-"; constr:constr; "in"; prim:var
| IDENT "apply"; "<-"; constr:constr
| IDENT "apply"; "->"; constr:constr; "in"; prim:var
| IDENT "apply"; "->"; constr:constr
| IDENT "apply"; LIST1 constr_with_bindings_arg SEP ","; in_hyp_as
| IDENT "eapply"; LIST1 constr_with_bindings_arg SEP ","; in_hyp_as
| IDENT "elim"; constr_with_bindings_arg; OPT eliminator
| IDENT "eelim"; constr_with_bindings_arg; OPT eliminator
| IDENT "case"; induction_clause_list
| IDENT "ecase"; induction_clause_list
| "fix"; prim:ident; prim:natural; "with"; LIST1 fixdecl
| "fix"; prim:ident; prim:natural
| "cofix"; prim:ident; "with"; LIST1 cofixdecl
| "cofix"; prim:ident
| IDENT "set"; bindings_with_parameters; tactic:clause
| IDENT "set"; constr:constr; as_name; tactic:clause
| IDENT "eset"; bindings_with_parameters; tactic:clause
| IDENT "eset"; constr:constr; as_name; tactic:clause
| IDENT "remember"; constr:constr; as_name; eqn_ipat; clause_dft_all
| IDENT "eremember"; constr:constr; as_name; eqn_ipat; clause_dft_all
| IDENT "assert"; lpar_id_coloneq; "("; Prim.identref; ":=";
constr:lconstr; ")"
| IDENT "assert"; tactic:test_lpar_id_colon; "("; Prim.identref; ":";
constr:lconstr; ")"; by_tactic
| IDENT "assert"; constr:constr; as_ipat; by_tactic
| IDENT "eassert"; lpar_id_coloneq; "("; Prim.identref; ":=";
constr:lconstr; ")"
| IDENT "eassert"; tactic:test_lpar_id_colon; "("; Prim.identref; ":";
constr:lconstr; ")"; by_tactic
| IDENT "eassert"; constr:constr; as_ipat; by_tactic
| IDENT "pose"; IDENT "proof"; lpar_id_coloneq; "("; Prim.identref; ":=";
constr:lconstr; ")"
| IDENT "pose"; IDENT "proof"; constr:lconstr; as_ipat
| IDENT "pose"; bindings_with_parameters
| IDENT "pose"; constr:constr; as_name
| IDENT "epose"; IDENT "proof"; lpar_id_coloneq; "("; Prim.identref; ":=";
constr:lconstr; ")"
| IDENT "epose"; IDENT "proof"; constr:lconstr; as_ipat
| IDENT "epose"; bindings_with_parameters
| IDENT "epose"; constr:constr; as_name
| IDENT "enough"; tactic:test_lpar_id_colon; "("; Prim.identref; ":";
constr:lconstr; ")"; by_tactic
| IDENT "enough"; constr:constr; as_ipat; by_tactic
| IDENT "eenough"; tactic:test_lpar_id_colon; "("; Prim.identref; ":";
constr:lconstr; ")"; by_tactic
| IDENT "eenough"; constr:constr; as_ipat; by_tactic
| IDENT "generalize"; IDENT "dependent"; constr:constr
| IDENT "generalize"; constr:constr; LIST1 constr:constr
| IDENT "generalize"; constr:constr; lookup_at_as_comma; occs; as_name;
LIST0 [ ","; pattern_occ; as_name ]
| IDENT "generalize"; constr:constr
| IDENT "induction"; induction_clause_list
| IDENT "einduction"; induction_clause_list
| IDENT "destruct"; induction_clause_list
| IDENT "edestruct"; induction_clause_list
| IDENT "rewrite"; "*"; tactic:orient; tactic:uconstr; "in"; prim:var;
"at"; tactic:occurrences; tactic:by_arg_tac
| IDENT "rewrite"; "*"; tactic:orient; tactic:uconstr; "in"; prim:var;
tactic:by_arg_tac
| IDENT "rewrite"; "*"; tactic:orient; tactic:uconstr; "at";
tactic:occurrences; "in"; prim:var; tactic:by_arg_tac
| IDENT "rewrite"; "*"; tactic:orient; tactic:uconstr; "at";
tactic:occurrences; tactic:by_arg_tac
| IDENT "rewrite"; "*"; tactic:orient; tactic:uconstr; tactic:by_arg_tac
| IDENT "rewrite"; LIST1 oriented_rewriter SEP ","; tactic:clause;
by_tactic
| IDENT "erewrite"; LIST1 oriented_rewriter SEP ","; tactic:clause;
by_tactic
| IDENT "dependent"; IDENT "induction"; prim:ident
| IDENT "dependent"; IDENT "generalize_eqs_vars"; prim:var
| IDENT "dependent"; IDENT "generalize_eqs"; prim:var
| IDENT "dependent"; IDENT "rewrite"; tactic:orient; constr:constr; "in";
prim:var
| IDENT "dependent"; IDENT "rewrite"; tactic:orient; constr:constr
| IDENT "dependent";
[ IDENT "simple"; IDENT "inversion" | IDENT "inversion"
| IDENT "inversion_clear" ]; tactic:quantified_hypothesis;
as_or_and_ipat; OPT [ "with"; constr:constr ]
| IDENT "simple"; IDENT "subst"
| IDENT "simple"; IDENT "notypeclasses"; IDENT "refine"; tactic:uconstr
| IDENT "simple"; IDENT "refine"; tactic:uconstr
| IDENT "simple"; IDENT "injection"; tactic:destruction_arg
| IDENT "simple"; IDENT "injection"
| IDENT "simple"; IDENT "destruct"; tactic:quantified_hypothesis
| IDENT "simple"; IDENT "induction"; tactic:quantified_hypothesis
| IDENT "simple"; IDENT "apply"; LIST1 constr_with_bindings_arg SEP ",";
in_hyp_as
| IDENT "simple"; IDENT "eapply"; LIST1 constr_with_bindings_arg SEP ",";
in_hyp_as
| IDENT "simple"; IDENT "inversion"; tactic:quantified_hypothesis;
as_or_and_ipat; in_hyp_list
| IDENT "inversion_clear"; tactic:quantified_hypothesis; as_or_and_ipat;
in_hyp_list
| IDENT "inversion"; tactic:quantified_hypothesis; "using"; constr:constr;
in_hyp_list
| IDENT "inversion"; tactic:quantified_hypothesis; as_or_and_ipat;
in_hyp_list
| IDENT "red"; tactic:clause
| IDENT "hnf"; tactic:clause
| IDENT "simpl"; delta_flag; OPT ref_or_pattern_occ; tactic:clause
| IDENT "cbv"; strategy_flag; tactic:clause
| IDENT "cbn"; strategy_flag; tactic:clause
| IDENT "lazy"; strategy_flag; tactic:clause
| IDENT "compute"; delta_flag; tactic:clause
| IDENT "vm_compute"; OPT ref_or_pattern_occ; tactic:clause
| IDENT "native_compute"; OPT ref_or_pattern_occ; tactic:clause
| IDENT "unfold"; LIST1 unfold_occ SEP ","; tactic:clause
| IDENT "fold"; LIST1 constr:constr; tactic:clause
| IDENT "pattern"; LIST1 pattern_occ SEP ","; tactic:clause
| IDENT "change"; conversion; tactic:clause
| IDENT "change_no_check"; conversion; tactic:clause ] ]
Entry tactic:tactic_arg is
[ LEFTA
[ IDENT "firstorder_using"; ":"; "("; tactic:firstorder_using; ")"
| IDENT "fresh"; LIST0 fresh_id
| IDENT "type_term"; tactic:uconstr
| IDENT "numgoals"
| IDENT "rewstrategy"; ":"; "("; tactic:rewstrategy; ")"
| IDENT "glob_constr_with_bindings"; ":"; "("; tactic:constr_with_bindings;
")"
| IDENT "eauto_search_strategy"; ":"; "("; tactic:eauto_search_strategy;
")"
| IDENT "eauto_search_strategy_name"; ":"; "(";
tactic:eauto_search_strategy_name; ")"
| IDENT "debug"; ":"; "("; tactic:debug; ")"
| IDENT "opthints"; ":"; "("; tactic:opthints; ")"
| IDENT "hints_path"; ":"; "("; tactic:hints_path; ")"
| IDENT "hints_path_atom"; ":"; "("; tactic:hints_path_atom; ")"
| IDENT "auto_using"; ":"; "("; tactic:auto_using; ")"
| IDENT "hintbases"; ":"; "("; tactic:hintbases; ")"
| IDENT "test"; ":"; "("; tactic:test; ")"
| IDENT "comparison"; ":"; "("; tactic:comparison; ")"
| IDENT "strategy_level_or_var"; ":"; "("; tactic:strategy_level_or_var;
")"
| IDENT "strategy_level"; ":"; "("; prim:strategy_level; ")"
| IDENT "test_lpar_id_colon"; ":"; "("; tactic:test_lpar_id_colon; ")"
| IDENT "in_clause"; ":"; "("; tactic:in_clause; ")"
| IDENT "by_arg_tac"; ":"; "("; tactic:by_arg_tac; ")"
| IDENT "rename"; ":"; "("; tactic:rename; ")"
| IDENT "hloc"; ":"; "("; tactic:hloc; ")"
| IDENT "casted_constr"; ":"; "("; constr:constr; ")"
| IDENT "lglob"; ":"; "("; constr:lconstr; ")"
| IDENT "lconstr"; ":"; "("; constr:lconstr; ")"
| IDENT "glob"; ":"; "("; constr:constr; ")"
| IDENT "occurrences"; ":"; "("; tactic:occurrences; ")"
| IDENT "natural"; ":"; "("; prim:natural; ")"
| IDENT "orient"; ":"; "("; tactic:orient; ")"
| IDENT "ltac"; ":"; "("; tactic:tactic_expr LEVEL "5"; ")"
| IDENT "open_constr"; ":"; "("; constr:lconstr; ")"
| IDENT "ipattern"; ":"; "("; tactic:simple_intropattern; ")"
| IDENT "constr"; ":"; "("; constr:lconstr; ")"
| IDENT "uconstr"; ":"; "("; constr:lconstr; ")"
| IDENT "reference"; ":"; "("; prim:reference; ")"
| IDENT "ident"; ":"; "("; prim:ident; ")"
| IDENT "smart_global"; ":"; "("; smart_global; ")"
| IDENT "string"; ":"; "("; prim:string; ")"
| IDENT "integer"; ":"; "("; prim:integer; ")"
| tactic:constr_eval ] ]
<prompt>Coq < 3 || 0 < </prompt>Add Search Blacklist "Private_" "_subproof".
<prompt>Coq < 4 || 0 < </prompt>Set Suggest Proof Using.
<prompt>Coq < 5 || 0 < </prompt>Set Diffs "off".
<prompt>Coq < 6 || 0 < </prompt>Redirect "/tmp/coqqX4oFL" Print Ltac Signatures.
<prompt>Coq < 7 || 0 < </prompt>Timeout 1 Print Grammar tactic.
Entry tactic:tactic_expr is
[ "5" RIGHTA
[ tactic:binder_tactic ]
| "4" LEFTA
[ SELF; ";"; tactic:binder_tactic
| SELF; ";"; SELF
| SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ]
| "3" RIGHTA
[ IDENT "try"; SELF
| IDENT "do"; tactic:int_or_var; SELF
| IDENT "timeout"; tactic:int_or_var; SELF
| IDENT "time"; OPT prim:string; SELF
| IDENT "repeat"; SELF
| IDENT "progress"; SELF
| IDENT "once"; SELF
| IDENT "exactly_once"; SELF
| IDENT "infoH"; SELF
| IDENT "abstract"; NEXT; "using"; constr:ident
| IDENT "abstract"; NEXT
| selector; SELF ]
| "2" RIGHTA
[ SELF; "+"; tactic:binder_tactic
| SELF; "+"; SELF
| SELF; "||"; tactic:binder_tactic
| SELF; "||"; SELF
| IDENT "tryif"; SELF; "then"; SELF; "else"; SELF ]
| "1" RIGHTA
[ IDENT "first"; "["; LIST0 tactic:tactic_expr SEP "|"; "]"
| IDENT "solve"; "["; LIST0 tactic:tactic_expr SEP "|"; "]"
| IDENT "idtac"; LIST0 message_token
| match_key; IDENT "goal"; "with"; match_context_list; "end"
| match_key; IDENT "reverse"; IDENT "goal"; "with"; match_context_list;
"end"
| match_key; SELF; "with"; match_list; "end"
| failkw; [ tactic:int_or_var | ]; LIST0 message_token
| tactic:simple_tactic
| tactic:tactic_arg
| prim:reference; LIST0 tactic_arg_compat ]
| "0" LEFTA
[ "("; SELF; ")"
| "["; ">"; tactic_then_gen; "]"
| tactic_atom ] ]
Entry tactic:binder_tactic is
[ RIGHTA
[ "fun"; LIST1 input_fun; "=>"; tactic:tactic_expr LEVEL "5"
| "let"; [ IDENT "rec" | ]; LIST1 let_clause SEP "with"; "in";
tactic:tactic_expr LEVEL "5"
| IDENT "info"; tactic:tactic_expr LEVEL "5" ] ]
Entry tactic:simple_tactic is
[ LEFTA
[ IDENT "gintuition"; OPT tactic:tactic
| IDENT "firstorder"; OPT tactic:tactic; "with"; LIST1 prim:preident
| IDENT "firstorder"; OPT tactic:tactic; tactic:firstorder_using; "with";
LIST1 prim:preident
| IDENT "firstorder"; OPT tactic:tactic; tactic:firstorder_using
| IDENT "congruence"; "with"; LIST1 constr:constr
| IDENT "congruence"; prim:integer; "with"; LIST1 constr:constr
| IDENT "congruence"; prim:integer
| IDENT "congruence"
| IDENT "dintuition"; tactic:tactic
| IDENT "dintuition"
| IDENT "intuition"; tactic:tactic
| IDENT "intuition"
| IDENT "assert_fails"; tactic:tactic_expr LEVEL "3"
| IDENT "assert_succeeds"; tactic:tactic_expr LEVEL "3"
| IDENT "now"; tactic:tactic
| IDENT "rewrite_all"; "<-"; constr:constr
| IDENT "rewrite_all"; constr:constr
| IDENT "destruct_with_eqn"; ":"; prim:ident; prim:ident
| IDENT "destruct_with_eqn"; ":"; prim:ident; constr:constr
| IDENT "destruct_with_eqn"; prim:ident
| IDENT "destruct_with_eqn"; constr:constr
| IDENT "decide"; IDENT "equality"
| IDENT "decide"; constr:constr; "with"; constr:constr
| IDENT "setoid_transitivity"; constr:constr
| IDENT "setoid_etransitivity"
| IDENT "setoid_symmetry"; "in"; prim:var
| IDENT "setoid_symmetry"
| IDENT "setoid_rewrite"; tactic:orient; tactic:constr_with_bindings; "at";
tactic:occurrences; "in"; prim:var
| IDENT "setoid_rewrite"; tactic:orient; tactic:constr_with_bindings; "at";
tactic:occurrences
| IDENT "setoid_rewrite"; tactic:orient; tactic:constr_with_bindings; "in";
prim:var; "at"; tactic:occurrences
| IDENT "setoid_rewrite"; tactic:orient; tactic:constr_with_bindings; "in";
prim:var
| IDENT "setoid_rewrite"; tactic:orient; tactic:constr_with_bindings
| IDENT "substitute"; tactic:orient; tactic:constr_with_bindings
| IDENT "rewrite_strat"; tactic:rewstrategy; "in"; prim:var
| IDENT "rewrite_strat"; tactic:rewstrategy
| IDENT "rewrite_db"; prim:preident; "in"; prim:var
| IDENT "rewrite_db"; prim:preident
| IDENT "progress_evars"; tactic:tactic
| IDENT "autoapply"; constr:constr; "using"; prim:preident
| IDENT "autoapply"; constr:constr; "with"; prim:preident
| IDENT "head_of_constr"; prim:ident; constr:constr
| IDENT "typeclasses"; IDENT "eauto"; IDENT "bfs"; OPT tactic:int_or_var;
"with"; LIST1 prim:preident
| IDENT "typeclasses"; IDENT "eauto"; OPT tactic:int_or_var; "with";
LIST1 prim:preident
| IDENT "typeclasses"; IDENT "eauto"; OPT tactic:int_or_var
| IDENT "unify"; constr:constr; constr:constr; "with"; prim:preident
| IDENT "unify"; constr:constr; constr:constr
| IDENT "autounfold_one"; tactic:hintbases; "in"; prim:var
| IDENT "autounfold_one"; tactic:hintbases
| IDENT "autounfold"; tactic:hintbases; tactic:clause
| IDENT "dfs"; IDENT "eauto"; OPT tactic:int_or_var; tactic:auto_using;
tactic:hintbases
| IDENT "info_eauto"; OPT tactic:int_or_var; OPT tactic:int_or_var;
tactic:auto_using; tactic:hintbases
| IDENT "new"; IDENT "auto"; OPT tactic:int_or_var; tactic:auto_using;
tactic:hintbases
| IDENT "eauto"; OPT tactic:int_or_var; OPT tactic:int_or_var;
tactic:auto_using; tactic:hintbases
| IDENT "prolog"; "["; LIST0 tactic:uconstr; "]"; tactic:int_or_var
| IDENT "info_auto"; OPT tactic:int_or_var; tactic:auto_using;
tactic:hintbases
| IDENT "auto"; OPT tactic:int_or_var; tactic:auto_using; tactic:hintbases
| IDENT "debug"; IDENT "eauto"; OPT tactic:int_or_var;
OPT tactic:int_or_var; tactic:auto_using; tactic:hintbases
| IDENT "debug"; IDENT "auto"; OPT tactic:int_or_var; tactic:auto_using;
tactic:hintbases
| IDENT "debug"; IDENT "trivial"; tactic:auto_using; tactic:hintbases
| IDENT "info_trivial"; tactic:auto_using; tactic:hintbases
| IDENT "trivial"; tactic:auto_using; tactic:hintbases
| IDENT "finish_timing"; "("; prim:string; ")"; OPT prim:string
| IDENT "finish_timing"; OPT prim:string
| IDENT "restart_timer"; OPT prim:string
| IDENT "show"; IDENT "ltac"; IDENT "profile"; IDENT "cutoff"; prim:integer
| IDENT "show"; IDENT "ltac"; IDENT "profile"; prim:string
| IDENT "show"; IDENT "ltac"; IDENT "profile"
| IDENT "reset"; IDENT "ltac"; IDENT "profile"
| IDENT "stop"; IDENT "ltac"; IDENT "profiling"
| IDENT "start"; IDENT "ltac"; IDENT "profiling"
| IDENT "with_strategy"; tactic:strategy_level_or_var; "[";
LIST1 smart_global; "]"; tactic:tactic_expr LEVEL "3"
| IDENT "guard"; tactic:test
| IDENT "swap"; tactic:int_or_var; tactic:int_or_var
| IDENT "cycle"; tactic:int_or_var
| IDENT "unshelve"; tactic:tactic_expr LEVEL "1"
| IDENT "transparent_abstract"; tactic:tactic_expr LEVEL "3"; "using";
prim:ident
| IDENT "transparent_abstract"; tactic:tactic_expr LEVEL "3"
| IDENT "destauto"; "in"; prim:var
| IDENT "destauto"
| IDENT "hget_evar"; tactic:int_or_var
| IDENT "hresolve_core"; "("; prim:ident; ":="; constr:constr; ")"; "at";
tactic:int_or_var; "in"; constr:constr
| IDENT "hresolve_core"; "("; prim:ident; ":="; constr:constr; ")"; "in";
constr:constr
| IDENT "specialize_eqs"; prim:var
| IDENT "generalize_eqs_vars"; prim:var
| IDENT "generalize_eqs"; prim:var
| IDENT "stepr"; constr:constr; "by"; tactic:tactic
| IDENT "stepr"; constr:constr
| IDENT "stepl"; constr:constr; "by"; tactic:tactic
| IDENT "stepl"; constr:constr
| IDENT "instantiate"; "("; prim:ident; ":="; constr:lconstr; ")"
| IDENT "instantiate"; "("; prim:integer; ":="; constr:lconstr; ")";
tactic:hloc
| IDENT "instantiate"
| IDENT "evar"; tactic:test_lpar_id_colon; "("; prim:ident; ":";
constr:lconstr; ")"
| IDENT "evar"; constr:constr
| IDENT "subst"; LIST1 prim:var
| IDENT "subst"
| IDENT "notypeclasses"; IDENT "refine"; tactic:uconstr
| IDENT "refine"; tactic:uconstr
| IDENT "autorewrite"; "*"; "with"; LIST1 prim:preident; tactic:clause;
"using"; tactic:tactic
| IDENT "autorewrite"; "*"; "with"; LIST1 prim:preident; tactic:clause
| IDENT "autorewrite"; "with"; LIST1 prim:preident; tactic:clause; "using";
tactic:tactic
| IDENT "autorewrite"; "with"; LIST1 prim:preident; tactic:clause
| IDENT "contradiction"; OPT tactic:constr_with_bindings
| IDENT "decompose"; "["; LIST1 constr:constr; "]"; constr:constr
| IDENT "decompose"; IDENT "record"; constr:constr
| IDENT "decompose"; IDENT "sum"; constr:constr
| IDENT "cutrewrite"; tactic:orient; constr:constr; "in"; prim:var
| IDENT "cutrewrite"; tactic:orient; constr:constr
| IDENT "einjection"; "as"; LIST0 tactic:simple_intropattern
| IDENT "einjection"; tactic:destruction_arg; "as";
LIST0 tactic:simple_intropattern
| IDENT "einjection"; tactic:destruction_arg
| IDENT "einjection"
| IDENT "injection"; "as"; LIST0 tactic:simple_intropattern
| IDENT "injection"; tactic:destruction_arg; "as";
LIST0 tactic:simple_intropattern
| IDENT "injection"; tactic:destruction_arg
| IDENT "injection"
| IDENT "ediscriminate"; tactic:destruction_arg
| IDENT "ediscriminate"
| IDENT "discriminate"; tactic:destruction_arg
| IDENT "discriminate"
| IDENT "esimplify_eq"; tactic:destruction_arg
| IDENT "esimplify_eq"
| IDENT "simplify_eq"; tactic:destruction_arg
| IDENT "simplify_eq"
| IDENT "replace"; "<-"; tactic:uconstr; tactic:clause
| IDENT "replace"; "->"; tactic:uconstr; tactic:clause
| IDENT "replace"; tactic:uconstr; "with"; constr:constr; tactic:clause;
tactic:by_arg_tac
| IDENT "replace"; tactic:uconstr; tactic:clause
| IDENT "clearbody"; LIST1 prim:var
| IDENT "clear"; IDENT "dependent"; prim:var
| IDENT "clear"; "-"; LIST1 prim:var
| IDENT "clear"; LIST0 prim:var
| IDENT "double"; IDENT "induction"; tactic:quantified_hypothesis;
tactic:quantified_hypothesis
| IDENT "revert"; IDENT "dependent"; prim:var
| IDENT "revert"; LIST1 prim:var
| IDENT "rename"; LIST1 tactic:rename SEP ","
| IDENT "move"; prim:var; "at"; IDENT "top"
| IDENT "move"; prim:var; "at"; IDENT "bottom"
| IDENT "move"; prim:var; IDENT "after"; prim:var
| IDENT "move"; prim:var; IDENT "before"; prim:var
| IDENT "intro"; "at"; IDENT "top"
| IDENT "intro"; "at"; IDENT "bottom"
| IDENT "intro"; IDENT "after"; prim:var
| IDENT "intro"; IDENT "before"; prim:var
| IDENT "intro"; prim:ident; "at"; IDENT "top"
| IDENT "intro"; prim:ident; "at"; IDENT "bottom"
| IDENT "intro"; prim:ident; IDENT "after"; prim:var
| IDENT "intro"; prim:ident; IDENT "before"; prim:var
| IDENT "intro"; prim:ident
| IDENT "intro"
| IDENT "eexists"; LIST1 tactic:bindings SEP ","
| IDENT "eexists"
| "exists"; LIST1 tactic:bindings SEP ","
| "exists"
| IDENT "esplit"; "with"; tactic:bindings
| IDENT "split"; "with"; tactic:bindings
| IDENT "symmetry"; "in"; tactic:in_clause
| IDENT "specialize"; tactic:constr_with_bindings; "as";
tactic:simple_intropattern
| IDENT "specialize"; tactic:constr_with_bindings
| IDENT "econstructor"; tactic:int_or_var; "with"; tactic:bindings
| IDENT "econstructor"; tactic:int_or_var
| IDENT "econstructor"
| IDENT "constructor"; tactic:int_or_var; "with"; tactic:bindings
| IDENT "constructor"; tactic:int_or_var
| IDENT "constructor"
| IDENT "eright"; "with"; tactic:bindings
| IDENT "right"; "with"; tactic:bindings
| IDENT "eleft"; "with"; tactic:bindings
| IDENT "left"; "with"; tactic:bindings
| IDENT "exact"; constr:constr
| IDENT "intros"; IDENT "until"; tactic:quantified_hypothesis
| IDENT "intros"; ne_intropatterns
| IDENT "intros"
| IDENT "eintros"; ne_intropatterns
| IDENT "eintros"
| IDENT "apply"; "<-"; constr:constr; "in"; prim:var
| IDENT "apply"; "<-"; constr:constr
| IDENT "apply"; "->"; constr:constr; "in"; prim:var
| IDENT "apply"; "->"; constr:constr
| IDENT "apply"; LIST1 constr_with_bindings_arg SEP ","; in_hyp_as
| IDENT "eapply"; LIST1 constr_with_bindings_arg SEP ","; in_hyp_as
| IDENT "elim"; constr_with_bindings_arg; OPT eliminator
| IDENT "eelim"; constr_with_bindings_arg; OPT eliminator
| IDENT "case"; induction_clause_list
| IDENT "ecase"; induction_clause_list
| "fix"; prim:ident; prim:natural; "with"; LIST1 fixdecl
| "fix"; prim:ident; prim:natural
| "cofix"; prim:ident; "with"; LIST1 cofixdecl
| "cofix"; prim:ident
| IDENT "set"; bindings_with_parameters; tactic:clause
| IDENT "set"; constr:constr; as_name; tactic:clause
| IDENT "eset"; bindings_with_parameters; tactic:clause
| IDENT "eset"; constr:constr; as_name; tactic:clause
| IDENT "remember"; constr:constr; as_name; eqn_ipat; clause_dft_all
| IDENT "eremember"; constr:constr; as_name; eqn_ipat; clause_dft_all
| IDENT "assert"; lpar_id_coloneq; "("; Prim.identref; ":=";
constr:lconstr; ")"
| IDENT "assert"; tactic:test_lpar_id_colon; "("; Prim.identref; ":";
constr:lconstr; ")"; by_tactic
| IDENT "assert"; constr:constr; as_ipat; by_tactic
| IDENT "eassert"; lpar_id_coloneq; "("; Prim.identref; ":=";
constr:lconstr; ")"
| IDENT "eassert"; tactic:test_lpar_id_colon; "("; Prim.identref; ":";
constr:lconstr; ")"; by_tactic
| IDENT "eassert"; constr:constr; as_ipat; by_tactic
| IDENT "pose"; IDENT "proof"; lpar_id_coloneq; "("; Prim.identref; ":=";
constr:lconstr; ")"
| IDENT "pose"; IDENT "proof"; constr:lconstr; as_ipat
| IDENT "pose"; bindings_with_parameters
| IDENT "pose"; constr:constr; as_name
| IDENT "epose"; IDENT "proof"; lpar_id_coloneq; "("; Prim.identref; ":=";
constr:lconstr; ")"
| IDENT "epose"; IDENT "proof"; constr:lconstr; as_ipat
| IDENT "epose"; bindings_with_parameters
| IDENT "epose"; constr:constr; as_name
| IDENT "enough"; tactic:test_lpar_id_colon; "("; Prim.identref; ":";
constr:lconstr; ")"; by_tactic
| IDENT "enough"; constr:constr; as_ipat; by_tactic
| IDENT "eenough"; tactic:test_lpar_id_colon; "("; Prim.identref; ":";
constr:lconstr; ")"; by_tactic
| IDENT "eenough"; constr:constr; as_ipat; by_tactic
| IDENT "generalize"; IDENT "dependent"; constr:constr
| IDENT "generalize"; constr:constr; LIST1 constr:constr
| IDENT "generalize"; constr:constr; lookup_at_as_comma; occs; as_name;
LIST0 [ ","; pattern_occ; as_name ]
| IDENT "generalize"; constr:constr
| IDENT "induction"; induction_clause_list
| IDENT "einduction"; induction_clause_list
| IDENT "destruct"; induction_clause_list
| IDENT "edestruct"; induction_clause_list
| IDENT "rewrite"; "*"; tactic:orient; tactic:uconstr; "in"; prim:var;
"at"; tactic:occurrences; tactic:by_arg_tac
| IDENT "rewrite"; "*"; tactic:orient; tactic:uconstr; "in"; prim:var;
tactic:by_arg_tac
| IDENT "rewrite"; "*"; tactic:orient; tactic:uconstr; "at";
tactic:occurrences; "in"; prim:var; tactic:by_arg_tac
| IDENT "rewrite"; "*"; tactic:orient; tactic:uconstr; "at";
tactic:occurrences; tactic:by_arg_tac
| IDENT "rewrite"; "*"; tactic:orient; tactic:uconstr; tactic:by_arg_tac
| IDENT "rewrite"; LIST1 oriented_rewriter SEP ","; tactic:clause;
by_tactic
| IDENT "erewrite"; LIST1 oriented_rewriter SEP ","; tactic:clause;
by_tactic
| IDENT "dependent"; IDENT "induction"; prim:ident
| IDENT "dependent"; IDENT "generalize_eqs_vars"; prim:var
| IDENT "dependent"; IDENT "generalize_eqs"; prim:var
| IDENT "dependent"; IDENT "rewrite"; tactic:orient; constr:constr; "in";
prim:var
| IDENT "dependent"; IDENT "rewrite"; tactic:orient; constr:constr
| IDENT "dependent";
[ IDENT "simple"; IDENT "inversion" | IDENT "inversion"
| IDENT "inversion_clear" ]; tactic:quantified_hypothesis;
as_or_and_ipat; OPT [ "with"; constr:constr ]
| IDENT "simple"; IDENT "subst"
| IDENT "simple"; IDENT "notypeclasses"; IDENT "refine"; tactic:uconstr
| IDENT "simple"; IDENT "refine"; tactic:uconstr
| IDENT "simple"; IDENT "injection"; tactic:destruction_arg
| IDENT "simple"; IDENT "injection"
| IDENT "simple"; IDENT "destruct"; tactic:quantified_hypothesis
| IDENT "simple"; IDENT "induction"; tactic:quantified_hypothesis
| IDENT "simple"; IDENT "apply"; LIST1 constr_with_bindings_arg SEP ",";
in_hyp_as
| IDENT "simple"; IDENT "eapply"; LIST1 constr_with_bindings_arg SEP ",";
in_hyp_as
| IDENT "simple"; IDENT "inversion"; tactic:quantified_hypothesis;
as_or_and_ipat; in_hyp_list
| IDENT "inversion_clear"; tactic:quantified_hypothesis; as_or_and_ipat;
in_hyp_list
| IDENT "inversion"; tactic:quantified_hypothesis; "using"; constr:constr;
in_hyp_list
| IDENT "inversion"; tactic:quantified_hypothesis; as_or_and_ipat;
in_hyp_list
| IDENT "red"; tactic:clause
| IDENT "hnf"; tactic:clause
| IDENT "simpl"; delta_flag; OPT ref_or_pattern_occ; tactic:clause
| IDENT "cbv"; strategy_flag; tactic:clause
| IDENT "cbn"; strategy_flag; tactic:clause
| IDENT "lazy"; strategy_flag; tactic:clause
| IDENT "compute"; delta_flag; tactic:clause
| IDENT "vm_compute"; OPT ref_or_pattern_occ; tactic:clause
| IDENT "native_compute"; OPT ref_or_pattern_occ; tactic:clause
| IDENT "unfold"; LIST1 unfold_occ SEP ","; tactic:clause
| IDENT "fold"; LIST1 constr:constr; tactic:clause
| IDENT "pattern"; LIST1 pattern_occ SEP ","; tactic:clause
| IDENT "change"; conversion; tactic:clause
| IDENT "change_no_check"; conversion; tactic:clause ] ]
Entry tactic:tactic_arg is
[ LEFTA
[ IDENT "firstorder_using"; ":"; "("; tactic:firstorder_using; ")"
| IDENT "fresh"; LIST0 fresh_id
| IDENT "type_term"; tactic:uconstr
| IDENT "numgoals"
| IDENT "rewstrategy"; ":"; "("; tactic:rewstrategy; ")"
| IDENT "glob_constr_with_bindings"; ":"; "("; tactic:constr_with_bindings;
")"
| IDENT "eauto_search_strategy"; ":"; "("; tactic:eauto_search_strategy;
")"
| IDENT "eauto_search_strategy_name"; ":"; "(";
tactic:eauto_search_strategy_name; ")"
| IDENT "debug"; ":"; "("; tactic:debug; ")"
| IDENT "opthints"; ":"; "("; tactic:opthints; ")"
| IDENT "hints_path"; ":"; "("; tactic:hints_path; ")"
| IDENT "hints_path_atom"; ":"; "("; tactic:hints_path_atom; ")"
| IDENT "auto_using"; ":"; "("; tactic:auto_using; ")"
| IDENT "hintbases"; ":"; "("; tactic:hintbases; ")"
| IDENT "test"; ":"; "("; tactic:test; ")"
| IDENT "comparison"; ":"; "("; tactic:comparison; ")"
| IDENT "strategy_level_or_var"; ":"; "("; tactic:strategy_level_or_var;
")"
| IDENT "strategy_level"; ":"; "("; prim:strategy_level; ")"
| IDENT "test_lpar_id_colon"; ":"; "("; tactic:test_lpar_id_colon; ")"
| IDENT "in_clause"; ":"; "("; tactic:in_clause; ")"
| IDENT "by_arg_tac"; ":"; "("; tactic:by_arg_tac; ")"
| IDENT "rename"; ":"; "("; tactic:rename; ")"
| IDENT "hloc"; ":"; "("; tactic:hloc; ")"
| IDENT "casted_constr"; ":"; "("; constr:constr; ")"
| IDENT "lglob"; ":"; "("; constr:lconstr; ")"
| IDENT "lconstr"; ":"; "("; constr:lconstr; ")"
| IDENT "glob"; ":"; "("; constr:constr; ")"
| IDENT "occurrences"; ":"; "("; tactic:occurrences; ")"
| IDENT "natural"; ":"; "("; prim:natural; ")"
| IDENT "orient"; ":"; "("; tactic:orient; ")"
| IDENT "ltac"; ":"; "("; tactic:tactic_expr LEVEL "5"; ")"
| IDENT "open_constr"; ":"; "("; constr:lconstr; ")"
| IDENT "ipattern"; ":"; "("; tactic:simple_intropattern; ")"
| IDENT "constr"; ":"; "("; constr:lconstr; ")"
| IDENT "uconstr"; ":"; "("; constr:lconstr; ")"
| IDENT "reference"; ":"; "("; prim:reference; ")"
| IDENT "ident"; ":"; "("; prim:ident; ")"
| IDENT "smart_global"; ":"; "("; smart_global; ")"
| IDENT "string"; ":"; "("; prim:string; ")"
| IDENT "integer"; ":"; "("; prim:integer; ")"
| tactic:constr_eval ] ]
<prompt>Coq < 8 || 0 < </prompt>Add Search Blacklist "Raw" "Proofs".
<prompt>Coq < 9 || 0 < </prompt>Set Search Output Name Only.
<prompt>Coq < 10 || 0 < </prompt>Redirect "/tmp/coqiX5NEp" SearchPattern _.
<prompt>Coq < 11 || 0 < </prompt>Remove Search Blacklist "Raw" "Proofs".
<prompt>Coq < 12 || 0 < </prompt>Unset Search Output Name Only.
<prompt>Coq < 13 || 0 < </prompt>Timeout 1 Print LoadPath.
Logical Path / Physical path:
<> /home/clement/.opam/coq-8.12/lib/coq/user-contrib
mathcomp.ssreflect
/home/clement/.opam/coq-8.12/lib/coq/user-contrib/mathcomp/ssreflect
mathcomp /home/clement/.opam/coq-8.12/lib/coq/user-contrib/mathcomp
SimpleIO /home/clement/.opam/coq-8.12/lib/coq/user-contrib/SimpleIO
RegLang /home/clement/.opam/coq-8.12/lib/coq/user-contrib/RegLang
QuickChick /home/clement/.opam/coq-8.12/lib/coq/user-contrib/QuickChick
Ltac2 /home/clement/.opam/coq-8.12/lib/coq/user-contrib/Ltac2
ExtLib.Tactics
/home/clement/.opam/coq-8.12/lib/coq/user-contrib/ExtLib/Tactics
ExtLib.Structures
/home/clement/.opam/coq-8.12/lib/coq/user-contrib/ExtLib/Structures
ExtLib.Relations
/home/clement/.opam/coq-8.12/lib/coq/user-contrib/ExtLib/Relations
ExtLib.Recur /home/clement/.opam/coq-8.12/lib/coq/user-contrib/ExtLib/Recur
ExtLib.Programming
/home/clement/.opam/coq-8.12/lib/coq/user-contrib/ExtLib/Programming
ExtLib.Generic
/home/clement/.opam/coq-8.12/lib/coq/user-contrib/ExtLib/Generic
ExtLib.Data.Set
/home/clement/.opam/coq-8.12/lib/coq/user-contrib/ExtLib/Data/Set
ExtLib.Data.Monads
/home/clement/.opam/coq-8.12/lib/coq/user-contrib/ExtLib/Data/Monads
ExtLib.Data.Map
/home/clement/.opam/coq-8.12/lib/coq/user-contrib/ExtLib/Data/Map
ExtLib.Data.Graph
/home/clement/.opam/coq-8.12/lib/coq/user-contrib/ExtLib/Data/Graph
ExtLib.Data.Eq
/home/clement/.opam/coq-8.12/lib/coq/user-contrib/ExtLib/Data/Eq
ExtLib.Data /home/clement/.opam/coq-8.12/lib/coq/user-contrib/ExtLib/Data
ExtLib.Core /home/clement/.opam/coq-8.12/lib/coq/user-contrib/ExtLib/Core
ExtLib /home/clement/.opam/coq-8.12/lib/coq/user-contrib/ExtLib
Coq /home/clement/.opam/coq-8.12/lib/coq/theories
Coq.ssrsearch /home/clement/.opam/coq-8.12/lib/coq/theories/ssrsearch
Coq.ssrmatching /home/clement/.opam/coq-8.12/lib/coq/theories/ssrmatching
Coq.ssr /home/clement/.opam/coq-8.12/lib/coq/theories/ssr
Coq.setoid_ring /home/clement/.opam/coq-8.12/lib/coq/theories/setoid_ring
Coq.rtauto /home/clement/.opam/coq-8.12/lib/coq/theories/rtauto
Coq.omega /home/clement/.opam/coq-8.12/lib/coq/theories/omega
Coq.nsatz /home/clement/.opam/coq-8.12/lib/coq/theories/nsatz
Coq.micromega /home/clement/.opam/coq-8.12/lib/coq/theories/micromega
Coq.funind /home/clement/.opam/coq-8.12/lib/coq/theories/funind
Coq.extraction /home/clement/.opam/coq-8.12/lib/coq/theories/extraction
Coq.derive /home/clement/.opam/coq-8.12/lib/coq/theories/derive
Coq.btauto /home/clement/.opam/coq-8.12/lib/coq/theories/btauto
Coq.ZArith /home/clement/.opam/coq-8.12/lib/coq/theories/ZArith
Coq.Wellfounded /home/clement/.opam/coq-8.12/lib/coq/theories/Wellfounded
Coq.Vectors /home/clement/.opam/coq-8.12/lib/coq/theories/Vectors
Coq.Unicode /home/clement/.opam/coq-8.12/lib/coq/theories/Unicode
Coq.Structures /home/clement/.opam/coq-8.12/lib/coq/theories/Structures
Coq.Strings /home/clement/.opam/coq-8.12/lib/coq/theories/Strings
Coq.Sorting /home/clement/.opam/coq-8.12/lib/coq/theories/Sorting
Coq.Sets /home/clement/.opam/coq-8.12/lib/coq/theories/Sets
Coq.Setoids /home/clement/.opam/coq-8.12/lib/coq/theories/Setoids
Coq.Relations /home/clement/.opam/coq-8.12/lib/coq/theories/Relations
Coq.Reals.Cauchy /home/clement/.opam/coq-8.12/lib/coq/theories/Reals/Cauchy
Coq.Reals.Abstract
/home/clement/.opam/coq-8.12/lib/coq/theories/Reals/Abstract
Coq.Reals /home/clement/.opam/coq-8.12/lib/coq/theories/Reals
Coq.QArith /home/clement/.opam/coq-8.12/lib/coq/theories/QArith
Coq.Program /home/clement/.opam/coq-8.12/lib/coq/theories/Program
Coq.PArith /home/clement/.opam/coq-8.12/lib/coq/theories/PArith
Coq.Numbers.Natural.Peano
/home/clement/.opam/coq-8.12/lib/coq/theories/Numbers/Natural/Peano
Coq.Numbers.Natural.Binary
/home/clement/.opam/coq-8.12/lib/coq/theories/Numbers/Natural/Binary
Coq.Numbers.Natural.Abstract
/home/clement/.opam/coq-8.12/lib/coq/theories/Numbers/Natural/Abstract
Coq.Numbers.Natural
/home/clement/.opam/coq-8.12/lib/coq/theories/Numbers/Natural
Coq.Numbers.NatInt
/home/clement/.opam/coq-8.12/lib/coq/theories/Numbers/NatInt
Coq.Numbers.Integer.NatPairs
/home/clement/.opam/coq-8.12/lib/coq/theories/Numbers/Integer/NatPairs
Coq.Numbers.Integer.Binary
/home/clement/.opam/coq-8.12/lib/coq/theories/Numbers/Integer/Binary
Coq.Numbers.Integer.Abstract
/home/clement/.opam/coq-8.12/lib/coq/theories/Numbers/Integer/Abstract
Coq.Numbers.Integer
/home/clement/.opam/coq-8.12/lib/coq/theories/Numbers/Integer
Coq.Numbers.Cyclic.ZModulo
/home/clement/.opam/coq-8.12/lib/coq/theories/Numbers/Cyclic/ZModulo
Coq.Numbers.Cyclic.Int63
/home/clement/.opam/coq-8.12/lib/coq/theories/Numbers/Cyclic/Int63
Coq.Numbers.Cyclic.Int31
/home/clement/.opam/coq-8.12/lib/coq/theories/Numbers/Cyclic/Int31
Coq.Numbers.Cyclic.Abstract
/home/clement/.opam/coq-8.12/lib/coq/theories/Numbers/Cyclic/Abstract
Coq.Numbers.Cyclic
/home/clement/.opam/coq-8.12/lib/coq/theories/Numbers/Cyclic
Coq.Numbers /home/clement/.opam/coq-8.12/lib/coq/theories/Numbers
Coq.NArith /home/clement/.opam/coq-8.12/lib/coq/theories/NArith
Coq.MSets /home/clement/.opam/coq-8.12/lib/coq/theories/MSets
Coq.Logic /home/clement/.opam/coq-8.12/lib/coq/theories/Logic
Coq.Lists /home/clement/.opam/coq-8.12/lib/coq/theories/Lists
Coq.Init /home/clement/.opam/coq-8.12/lib/coq/theories/Init
Coq.Floats /home/clement/.opam/coq-8.12/lib/coq/theories/Floats
Coq.FSets /home/clement/.opam/coq-8.12/lib/coq/theories/FSets
Coq.Compat /home/clement/.opam/coq-8.12/lib/coq/theories/Compat
Coq.Classes /home/clement/.opam/coq-8.12/lib/coq/theories/Classes
Coq.Bool /home/clement/.opam/coq-8.12/lib/coq/theories/Bool
Coq.Arith /home/clement/.opam/coq-8.12/lib/coq/theories/Arith
<> /home/clement/documents/academia/faculty-applications
<prompt>Coq < 14 || 0 < </prompt>Set Printing Depth 50 .
<prompt>Coq < 15 || 0 < </prompt>Set Printing Width 68.
<prompt>Coq < 16 || 0 < </prompt>Check nat.
nat
: Set
<prompt>Coq < 17 || 0 < </prompt>
Looks good, no? The Set suggest proof using is in the middle.
from company-coq.
Matafou
commented on June 30, 2024
oops sorry you are right.
from company-coq.
Related Issues (20)
- company-coq-lemma-from-goal should be adapted w.r.t. Coq Diffs
- No match when installing this package from MELPA HOT 4
- `M-.` and notations HOT 1
- broken Layout when using Tex HOT 1
- Compile Before Require not working anymore HOT 2
- jump to definition: new window
- New subscript syntax? HOT 2
- company-coq-go-to-point fails HOT 11
- feature wish: highlight the corresponding hyp in the goals buffer when completing.
- new hyps not proposed for completion when in diff mode. HOT 6
- Completion becomes slower over time HOT 4
- jump to definition fails for constructors of Variants
- Tutorial outdated
- Incorrect use of Unicode symbol in error message for Coq HOT 1
- Is there a way to disable the documentation buffer? HOT 7
- Feedback from Coq Community Survey 2022.
- Improve (company-coq-occur) to cope with non-one-liner statements? HOT 2
- Requesting support for .vos (in addition to .vio) files HOT 2
- "SPP" for "Set Printing Parentheses" is useful, should be added. HOT 3
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from company-coq.