search

cpitclaudel / company-coq

A Coq IDE build on top of Proof General's Coq mode
GNU General Public License v3.0
351 stars 29 forks source link

Completion does not work on (some?) non-imported modules #95

Closed JasonGross closed 8 years ago

JasonGross commented 8 years ago

Here is a case where completion fails:

Require Coq.Lists.List.
Module Operations.
  Module Export List.
    Axiom foobar : Set.
  End List.
  Axiom bazqux : Set.
End Operations.

I can get completion for Goal List., but not Goal Operations.

image

image

image

cpitclaudel commented 8 years ago

8.5, right? I get the following in 8.4:

screenshot from 2016-03-02 13 50 45

JasonGross commented 8 years ago

No, this is 8.4pl6. I just updated company-coq and restarted emacs (24.3.1), and still don't get completions for Oper.

cpitclaudel commented 8 years ago

Are you using a patched coqtop?

cpitclaudel commented 8 years ago

It works on 8.5 as well for me. screenshot from 2016-03-02 13 59 50

JasonGross commented 8 years ago

The *coq* buffer is the following. Does that answer your question?

Welcome to Coq 8.4pl6 (February 2016)

<prompt>Coq < 1 || 0 < </prompt>Redirect "/tmp/coq30429aR1" Test Search Output Name Only.

<prompt>Coq < 2 || 0 < </prompt>Timeout 1 Print Grammar tactic.
Entry tactic_expr is
[ "5" RIGHTA
  [ tactic:binder_tactic ]
| "4" LEFTA
  [ SELF; ";"; "["; tactic_then_gen; "]"
  | SELF; ";"; tactic:binder_tactic
  | SELF; ";"; SELF ]
| "3" RIGHTA
  [ IDENT "try"; SELF
  | IDENT "do"; tactic:int_or_var; SELF
  | IDENT "timeout"; tactic:int_or_var; SELF
  | IDENT "repeat"; SELF
  | IDENT "progress"; SELF
  | IDENT "abstract"; NEXT; "using"; prim:ident
  | IDENT "abstract"; NEXT ]
| "2" RIGHTA
  [ SELF; "||"; tactic:binder_tactic
  | SELF; "||"; SELF ]
| "1" RIGHTA
  [ IDENT "first"; "["; LIST0 tactic:tactic_expr SEP "|"; "]"
  | IDENT "solve"; "["; LIST0 tactic:tactic_expr SEP "|"; "]"
  | IDENT "idtac"; LIST0 message_token
  | IDENT "fail"; [ tactic:int_or_var |  ]; LIST0 message_token
  | IDENT "external"; STRING; STRING; LIST1 tactic:tactic_arg
  | IDENT "constr"; ":"; METAIDENT
  | IDENT "constr"; ":"; constr:constr
  | IDENT "ipattern"; ":"; tactic:simple_intropattern
  | 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"
  | tactic:simple_tactic
  | may_eval_arg
  | prim:reference; LIST0 tactic:tactic_arg ]
| "0" LEFTA
  [ "("; SELF; ")"
  | tactic_atom ] ]
Entry 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 simple_tactic is
[ LEFTA
  [ 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 "poseq"; prim:ident; constr:constr
  | IDENT "fauto"; tactic:tactic
  | IDENT "fauto"
  | IDENT "finduction"; prim:ident; OPT prim:natural
  | IDENT "soft"; IDENT "functional"; IDENT "induction"; LIST1 constr:constr;
    tactic:fun_ind_using; tactic:with_names
  | IDENT "functional"; IDENT "induction"; LIST1 constr:constr;
    tactic:fun_ind_using; tactic:with_names
  | IDENT "functional"; IDENT "inversion"; tactic:quantified_hypothesis;
    OPT prim:reference
  | 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 "f_equal"
  | IDENT "congruence"; "with"; LIST1 constr:constr
  | IDENT "congruence"; prim:integer; "with"; LIST1 constr:constr
  | IDENT "congruence"; prim:integer
  | IDENT "congruence"
  | IDENT "stop"; IDENT "profiling"
  | IDENT "start"; IDENT "profiling"
  | IDENT "compare"; constr:constr; constr:constr
  | IDENT "decide"; IDENT "equality"
  | IDENT "decide"; constr:constr; "with"; constr:constr
  | IDENT "intuition"; tactic:tactic
  | IDENT "intuition"
  | IDENT "tauto"
  | IDENT "myapply"; constr:global; LIST0 constr:constr
  | IDENT "fold_matches"; constr:constr
  | IDENT "fold_match"; constr:constr
  | IDENT "implify"; prim:var
  | IDENT "setoid_transitivity"; constr:constr
  | IDENT "setoid_etransitivity"
  | IDENT "setoid_reflexivity"
  | IDENT "setoid_symmetry"; "in"; prim:var
  | IDENT "setoid_symmetry"
  | IDENT "rew"; tactic:orient; tactic:glob_constr_with_bindings; "in";
    prim:var; "at"; tactic:occurrences
  | IDENT "rew"; tactic:orient; tactic:glob_constr_with_bindings; "in";
    prim:var
  | IDENT "rew"; tactic:orient; tactic:glob_constr_with_bindings; "at";
    tactic:occurrences; "in"; prim:var
  | IDENT "rew"; tactic:orient; tactic:glob_constr_with_bindings; "at";
    tactic:occurrences
  | IDENT "rew"; tactic:orient; tactic:glob_constr_with_bindings
  | IDENT "setoid_rewrite"; tactic:orient; tactic:glob_constr_with_bindings;
    "at"; tactic:occurrences; "in"; prim:var
  | IDENT "setoid_rewrite"; tactic:orient; tactic:glob_constr_with_bindings;
    "at"; tactic:occurrences
  | IDENT "setoid_rewrite"; tactic:orient; tactic:glob_constr_with_bindings;
    "in"; prim:var; "at"; tactic:occurrences
  | IDENT "setoid_rewrite"; tactic:orient; tactic:glob_constr_with_bindings;
    "in"; prim:var
  | IDENT "setoid_rewrite"; tactic:orient; tactic:glob_constr_with_bindings
  | IDENT "substitute"; tactic:orient; tactic:glob_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 "autoapply"; constr:constr; "using"; prim:preident
  | IDENT "is_ground"; constr:constr
  | IDENT "not_evar"; constr:constr
  | IDENT "head_of_constr"; prim:ident; constr:constr
  | IDENT "typeclasses"; IDENT "eauto"; "with"; LIST1 prim:preident
  | IDENT "typeclasses"; IDENT "eauto"
  | IDENT "progress_evars"; tactic:tactic
  | IDENT "convert_concl_no_check"; constr:constr
  | IDENT "unify"; constr:constr; constr:constr; "with"; prim:preident
  | IDENT "unify"; constr:constr; constr:constr
  | IDENT "autounfoldify"; constr:constr
  | IDENT "autounfold_one"; tactic:hintbases; "in"; prim:var
  | IDENT "autounfold_one"; tactic:hintbases
  | IDENT "autounfold"; tactic:hintbases; tactic:in_arg_hyp
  | 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:open_constr; "]"; tactic:int_or_var
  | IDENT "eexact"; constr:constr
  | IDENT "eassumption"
  | IDENT "is_fix"; constr:constr
  | IDENT "is_var"; constr:constr
  | IDENT "has_evar"; constr:constr
  | IDENT "is_evar"; constr:constr
  | IDENT "constr_eq"; constr:constr; constr:constr
  | 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:integer; ":="; tactic:glob; ")";
    tactic:hloc
  | IDENT "instantiate"
  | IDENT "evar"; "("; prim:ident; ":"; constr:lconstr; ")"
  | IDENT "evar"; constr:constr
  | IDENT "subst"; LIST1 prim:var
  | IDENT "subst"
  | IDENT "refine"; tactic:casted_open_constr
  | IDENT "autorewrite"; "*"; "with"; LIST1 prim:preident; tactic:in_arg_hyp;
    "using"; tactic:tactic
  | IDENT "autorewrite"; "*"; "with"; LIST1 prim:preident; tactic:in_arg_hyp
  | IDENT "autorewrite"; "with"; LIST1 prim:preident; tactic:in_arg_hyp;
    "using"; tactic:tactic
  | IDENT "autorewrite"; "with"; LIST1 prim:preident; tactic:in_arg_hyp
  | IDENT "contradiction"; OPT tactic:constr_with_bindings
  | IDENT "absurd"; 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:quantified_hypothesis; "as";
    LIST0 tactic:simple_intropattern
  | IDENT "einjection"; tactic:quantified_hypothesis
  | IDENT "einjection"; tactic:constr_with_bindings; "as";
    LIST0 tactic:simple_intropattern
  | IDENT "einjection"; tactic:constr_with_bindings
  | IDENT "einjection"
  | IDENT "injection"; "as"; LIST0 tactic:simple_intropattern
  | IDENT "injection"; tactic:quantified_hypothesis; "as";
    LIST0 tactic:simple_intropattern
  | IDENT "injection"; tactic:quantified_hypothesis
  | IDENT "injection"; tactic:constr_with_bindings; "as";
    LIST0 tactic:simple_intropattern
  | IDENT "injection"; tactic:constr_with_bindings
  | IDENT "injection"
  | IDENT "ediscriminate"; tactic:quantified_hypothesis
  | IDENT "ediscriminate"; tactic:constr_with_bindings
  | IDENT "ediscriminate"
  | IDENT "discriminate"; tactic:quantified_hypothesis
  | IDENT "discriminate"; tactic:constr_with_bindings
  | IDENT "discriminate"
  | IDENT "esimplify_eq"; tactic:quantified_hypothesis
  | IDENT "esimplify_eq"; tactic:constr_with_bindings
  | IDENT "esimplify_eq"
  | IDENT "simplify_eq"; tactic:quantified_hypothesis
  | IDENT "simplify_eq"; tactic:constr_with_bindings
  | IDENT "simplify_eq"
  | IDENT "replace"; "<-"; tactic:open_constr; tactic:in_arg_hyp
  | IDENT "replace"; "->"; tactic:open_constr; tactic:in_arg_hyp
  | IDENT "replace"; tactic:open_constr; "with"; constr:constr; "at";
    tactic:occurrences; tactic:by_arg_tac
  | IDENT "replace"; tactic:open_constr; "with"; constr:constr;
    tactic:in_arg_hyp; tactic:by_arg_tac
  | IDENT "replace"; tactic:open_constr; tactic:in_arg_hyp
  | IDENT "admit"
  | IDENT "intros"; IDENT "until"; tactic:quantified_hypothesis
  | IDENT "intros"; intropatterns
  | IDENT "intro"; move_location
  | IDENT "intro"; prim:ident; move_location
  | IDENT "intro"; prim:ident
  | IDENT "intro"
  | IDENT "assumption"
  | IDENT "exact"; constr:constr
  | IDENT "exact_no_check"; constr:constr
  | IDENT "vm_cast_no_check"; constr:constr
  | 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 tactic:constr_with_bindings SEP ","; in_hyp_as
  | IDENT "eapply"; LIST1 tactic:constr_with_bindings SEP ","; in_hyp_as
  | IDENT "elim"; tactic:constr_with_bindings; OPT eliminator
  | IDENT "eelim"; tactic:constr_with_bindings; OPT eliminator
  | IDENT "elimtype"; constr:constr
  | IDENT "case"; induction_clause_list
  | IDENT "ecase"; induction_clause_list
  | IDENT "casetype"; constr:constr
  | "fix"; prim:natural
  | "fix"; prim:ident; prim:natural; "with"; LIST1 fixdecl
  | "fix"; prim:ident; prim:natural
  | "cofix"; prim:ident; "with"; LIST1 cofixdecl
  | "cofix"; prim:ident
  | "cofix"
  | IDENT "set"; bindings_with_parameters; clause_dft_concl
  | IDENT "set"; constr:constr; as_name; clause_dft_concl
  | IDENT "remember"; constr:constr; as_name; eqn_ipat; clause_dft_all
  | IDENT "assert"; lpar_id_coloneq; "("; Prim.identref; ":=";
    constr:lconstr; ")"
  | IDENT "assert"; lpar_id_colon; "("; Prim.identref; ":"; constr:lconstr;
    ")"; by_tactic
  | IDENT "assert"; constr:constr; as_ipat; by_tactic
  | IDENT "pose"; IDENT "proof"; constr:lconstr; as_ipat
  | IDENT "pose"; bindings_with_parameters
  | IDENT "pose"; constr:constr; as_name
  | IDENT "cut"; constr:constr
  | IDENT "generalize"; IDENT "dependent"; constr:constr
  | IDENT "generalize"; constr:constr; LIST1 constr:constr
  | IDENT "generalize"; constr:constr; lookup_at_as_coma; occs; as_name;
    LIST0 [ ","; pattern_occ; as_name ]
  | IDENT "generalize"; constr:constr
  | IDENT "specialize"; OPT prim:natural; tactic:constr_with_bindings
  | IDENT "lapply"; constr:constr
  | IDENT "induction"; induction_clause_list
  | IDENT "einduction"; induction_clause_list
  | IDENT "double"; IDENT "induction"; tactic:quantified_hypothesis;
    tactic:quantified_hypothesis
  | IDENT "destruct"; induction_clause_list
  | IDENT "edestruct"; induction_clause_list
  | IDENT "decompose"; IDENT "record"; constr:constr
  | IDENT "decompose"; IDENT "sum"; constr:constr
  | IDENT "decompose"; "["; LIST1 smart_global; "]"; constr:constr
  | IDENT "trivial"; auto_using; hintbases
  | IDENT "info_trivial"; auto_using; hintbases
  | IDENT "auto"; OPT tactic:int_or_var; auto_using; hintbases
  | IDENT "info_auto"; OPT tactic:int_or_var; auto_using; hintbases
  | IDENT "debug"; IDENT "eauto"; OPT tactic:int_or_var;
    OPT tactic:int_or_var; tactic:auto_using; tactic:hintbases
  | IDENT "debug"; IDENT "trivial"; auto_using; hintbases
  | IDENT "debug"; IDENT "auto"; OPT tactic:int_or_var; auto_using; hintbases
  | IDENT "clear"; IDENT "dependent"; prim:var
  | IDENT "clear"; "-"; LIST1 id_or_meta
  | IDENT "clear"; LIST0 id_or_meta
  | IDENT "clearbody"; LIST1 id_or_meta
  | IDENT "move"; id_or_meta; move_location
  | IDENT "rename"; LIST1 rename SEP ","
  | IDENT "revert"; IDENT "dependent"; prim:var
  | IDENT "revert"; LIST1 id_or_meta
  | IDENT "left"; with_bindings
  | IDENT "eleft"; with_bindings
  | IDENT "right"; with_bindings
  | IDENT "eright"; with_bindings
  | IDENT "split"; with_bindings
  | IDENT "esplit"; with_bindings
  | "exists"; LIST1 opt_bindings SEP ","
  | IDENT "eexists"; LIST1 opt_bindings SEP ","
  | IDENT "constructor"; nat_or_var; with_bindings
  | IDENT "constructor"; OPT tactic:tactic
  | IDENT "econstructor"; nat_or_var; with_bindings
  | IDENT "econstructor"; OPT tactic:tactic
  | IDENT "reflexivity"
  | IDENT "symmetry"; clause_dft_concl
  | IDENT "transitivity"; constr:constr
  | IDENT "etransitivity"
  | IDENT "rewrite"; "*"; tactic:orient; tactic:open_constr; "in"; prim:var;
    "at"; tactic:occurrences; tactic:by_arg_tac
  | IDENT "rewrite"; "*"; tactic:orient; tactic:open_constr; "in"; prim:var;
    tactic:by_arg_tac
  | IDENT "rewrite"; "*"; tactic:orient; tactic:open_constr; "at";
    tactic:occurrences; "in"; prim:var; tactic:by_arg_tac
  | IDENT "rewrite"; "*"; tactic:orient; tactic:open_constr; "at";
    tactic:occurrences; tactic:by_arg_tac
  | IDENT "rewrite"; "*"; tactic:orient; tactic:open_constr;
    tactic:by_arg_tac
  | IDENT "rewrite"; LIST1 oriented_rewriter SEP ","; clause_dft_concl;
    opt_by_tactic
  | IDENT "erewrite"; LIST1 oriented_rewriter SEP ","; clause_dft_concl;
    opt_by_tactic
  | 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;
    with_inversion_names; OPT [ "with"; constr:constr ]
  | IDENT "simple"; IDENT "subst"
  | IDENT "simple"; IDENT "apply"; LIST1 tactic:constr_with_bindings SEP ",";
    in_hyp_as
  | IDENT "simple"; IDENT "eapply";
    LIST1 tactic:constr_with_bindings SEP ","; in_hyp_as
  | IDENT "simple"; IDENT "induction"; tactic:quantified_hypothesis
  | IDENT "simple"; IDENT "destruct"; tactic:quantified_hypothesis
  | IDENT "simple"; IDENT "inversion"; tactic:quantified_hypothesis;
    with_inversion_names; in_hyp_list
  | IDENT "inversion_clear"; tactic:quantified_hypothesis;
    with_inversion_names; in_hyp_list
  | IDENT "inversion"; tactic:quantified_hypothesis; "using"; constr:constr;
    in_hyp_list
  | IDENT "inversion"; tactic:quantified_hypothesis; with_inversion_names;
    in_hyp_list
  | IDENT "change"; conversion; clause_dft_concl
  | red_tactic; clause_dft_concl ] ]

<prompt>Coq < 3 || 0 < </prompt>Add Search Blacklist "Private_" "_subproof". 

<prompt>Coq < 4 || 0 < </prompt>Redirect "/tmp/coq30429xzi" Print Ltac Signatures.

<prompt>Coq < 5 || 0 < </prompt>Timeout 1 Print Grammar tactic.
Entry tactic_expr is
[ "5" RIGHTA
  [ tactic:binder_tactic ]
| "4" LEFTA
  [ SELF; ";"; "["; tactic_then_gen; "]"
  | SELF; ";"; tactic:binder_tactic
  | SELF; ";"; SELF ]
| "3" RIGHTA
  [ IDENT "try"; SELF
  | IDENT "do"; tactic:int_or_var; SELF
  | IDENT "timeout"; tactic:int_or_var; SELF
  | IDENT "repeat"; SELF
  | IDENT "progress"; SELF
  | IDENT "abstract"; NEXT; "using"; prim:ident
  | IDENT "abstract"; NEXT ]
| "2" RIGHTA
  [ SELF; "||"; tactic:binder_tactic
  | SELF; "||"; SELF ]
| "1" RIGHTA
  [ IDENT "first"; "["; LIST0 tactic:tactic_expr SEP "|"; "]"
  | IDENT "solve"; "["; LIST0 tactic:tactic_expr SEP "|"; "]"
  | IDENT "idtac"; LIST0 message_token
  | IDENT "fail"; [ tactic:int_or_var |  ]; LIST0 message_token
  | IDENT "external"; STRING; STRING; LIST1 tactic:tactic_arg
  | IDENT "constr"; ":"; METAIDENT
  | IDENT "constr"; ":"; constr:constr
  | IDENT "ipattern"; ":"; tactic:simple_intropattern
  | 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"
  | tactic:simple_tactic
  | may_eval_arg
  | prim:reference; LIST0 tactic:tactic_arg ]
| "0" LEFTA
  [ "("; SELF; ")"
  | tactic_atom ] ]
Entry 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 simple_tactic is
[ LEFTA
  [ 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 "poseq"; prim:ident; constr:constr
  | IDENT "fauto"; tactic:tactic
  | IDENT "fauto"
  | IDENT "finduction"; prim:ident; OPT prim:natural
  | IDENT "soft"; IDENT "functional"; IDENT "induction"; LIST1 constr:constr;
    tactic:fun_ind_using; tactic:with_names
  | IDENT "functional"; IDENT "induction"; LIST1 constr:constr;
    tactic:fun_ind_using; tactic:with_names
  | IDENT "functional"; IDENT "inversion"; tactic:quantified_hypothesis;
    OPT prim:reference
  | 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 "f_equal"
  | IDENT "congruence"; "with"; LIST1 constr:constr
  | IDENT "congruence"; prim:integer; "with"; LIST1 constr:constr
  | IDENT "congruence"; prim:integer
  | IDENT "congruence"
  | IDENT "stop"; IDENT "profiling"
  | IDENT "start"; IDENT "profiling"
  | IDENT "compare"; constr:constr; constr:constr
  | IDENT "decide"; IDENT "equality"
  | IDENT "decide"; constr:constr; "with"; constr:constr
  | IDENT "intuition"; tactic:tactic
  | IDENT "intuition"
  | IDENT "tauto"
  | IDENT "myapply"; constr:global; LIST0 constr:constr
  | IDENT "fold_matches"; constr:constr
  | IDENT "fold_match"; constr:constr
  | IDENT "implify"; prim:var
  | IDENT "setoid_transitivity"; constr:constr
  | IDENT "setoid_etransitivity"
  | IDENT "setoid_reflexivity"
  | IDENT "setoid_symmetry"; "in"; prim:var
  | IDENT "setoid_symmetry"
  | IDENT "rew"; tactic:orient; tactic:glob_constr_with_bindings; "in";
    prim:var; "at"; tactic:occurrences
  | IDENT "rew"; tactic:orient; tactic:glob_constr_with_bindings; "in";
    prim:var
  | IDENT "rew"; tactic:orient; tactic:glob_constr_with_bindings; "at";
    tactic:occurrences; "in"; prim:var
  | IDENT "rew"; tactic:orient; tactic:glob_constr_with_bindings; "at";
    tactic:occurrences
  | IDENT "rew"; tactic:orient; tactic:glob_constr_with_bindings
  | IDENT "setoid_rewrite"; tactic:orient; tactic:glob_constr_with_bindings;
    "at"; tactic:occurrences; "in"; prim:var
  | IDENT "setoid_rewrite"; tactic:orient; tactic:glob_constr_with_bindings;
    "at"; tactic:occurrences
  | IDENT "setoid_rewrite"; tactic:orient; tactic:glob_constr_with_bindings;
    "in"; prim:var; "at"; tactic:occurrences
  | IDENT "setoid_rewrite"; tactic:orient; tactic:glob_constr_with_bindings;
    "in"; prim:var
  | IDENT "setoid_rewrite"; tactic:orient; tactic:glob_constr_with_bindings
  | IDENT "substitute"; tactic:orient; tactic:glob_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 "autoapply"; constr:constr; "using"; prim:preident
  | IDENT "is_ground"; constr:constr
  | IDENT "not_evar"; constr:constr
  | IDENT "head_of_constr"; prim:ident; constr:constr
  | IDENT "typeclasses"; IDENT "eauto"; "with"; LIST1 prim:preident
  | IDENT "typeclasses"; IDENT "eauto"
  | IDENT "progress_evars"; tactic:tactic
  | IDENT "convert_concl_no_check"; constr:constr
  | IDENT "unify"; constr:constr; constr:constr; "with"; prim:preident
  | IDENT "unify"; constr:constr; constr:constr
  | IDENT "autounfoldify"; constr:constr
  | IDENT "autounfold_one"; tactic:hintbases; "in"; prim:var
  | IDENT "autounfold_one"; tactic:hintbases
  | IDENT "autounfold"; tactic:hintbases; tactic:in_arg_hyp
  | 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:open_constr; "]"; tactic:int_or_var
  | IDENT "eexact"; constr:constr
  | IDENT "eassumption"
  | IDENT "is_fix"; constr:constr
  | IDENT "is_var"; constr:constr
  | IDENT "has_evar"; constr:constr
  | IDENT "is_evar"; constr:constr
  | IDENT "constr_eq"; constr:constr; constr:constr
  | 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:integer; ":="; tactic:glob; ")";
    tactic:hloc
  | IDENT "instantiate"
  | IDENT "evar"; "("; prim:ident; ":"; constr:lconstr; ")"
  | IDENT "evar"; constr:constr
  | IDENT "subst"; LIST1 prim:var
  | IDENT "subst"
  | IDENT "refine"; tactic:casted_open_constr
  | IDENT "autorewrite"; "*"; "with"; LIST1 prim:preident; tactic:in_arg_hyp;
    "using"; tactic:tactic
  | IDENT "autorewrite"; "*"; "with"; LIST1 prim:preident; tactic:in_arg_hyp
  | IDENT "autorewrite"; "with"; LIST1 prim:preident; tactic:in_arg_hyp;
    "using"; tactic:tactic
  | IDENT "autorewrite"; "with"; LIST1 prim:preident; tactic:in_arg_hyp
  | IDENT "contradiction"; OPT tactic:constr_with_bindings
  | IDENT "absurd"; 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:quantified_hypothesis; "as";
    LIST0 tactic:simple_intropattern
  | IDENT "einjection"; tactic:quantified_hypothesis
  | IDENT "einjection"; tactic:constr_with_bindings; "as";
    LIST0 tactic:simple_intropattern
  | IDENT "einjection"; tactic:constr_with_bindings
  | IDENT "einjection"
  | IDENT "injection"; "as"; LIST0 tactic:simple_intropattern
  | IDENT "injection"; tactic:quantified_hypothesis; "as";
    LIST0 tactic:simple_intropattern
  | IDENT "injection"; tactic:quantified_hypothesis
  | IDENT "injection"; tactic:constr_with_bindings; "as";
    LIST0 tactic:simple_intropattern
  | IDENT "injection"; tactic:constr_with_bindings
  | IDENT "injection"
  | IDENT "ediscriminate"; tactic:quantified_hypothesis
  | IDENT "ediscriminate"; tactic:constr_with_bindings
  | IDENT "ediscriminate"
  | IDENT "discriminate"; tactic:quantified_hypothesis
  | IDENT "discriminate"; tactic:constr_with_bindings
  | IDENT "discriminate"
  | IDENT "esimplify_eq"; tactic:quantified_hypothesis
  | IDENT "esimplify_eq"; tactic:constr_with_bindings
  | IDENT "esimplify_eq"
  | IDENT "simplify_eq"; tactic:quantified_hypothesis
  | IDENT "simplify_eq"; tactic:constr_with_bindings
  | IDENT "simplify_eq"
  | IDENT "replace"; "<-"; tactic:open_constr; tactic:in_arg_hyp
  | IDENT "replace"; "->"; tactic:open_constr; tactic:in_arg_hyp
  | IDENT "replace"; tactic:open_constr; "with"; constr:constr; "at";
    tactic:occurrences; tactic:by_arg_tac
  | IDENT "replace"; tactic:open_constr; "with"; constr:constr;
    tactic:in_arg_hyp; tactic:by_arg_tac
  | IDENT "replace"; tactic:open_constr; tactic:in_arg_hyp
  | IDENT "admit"
  | IDENT "intros"; IDENT "until"; tactic:quantified_hypothesis
  | IDENT "intros"; intropatterns
  | IDENT "intro"; move_location
  | IDENT "intro"; prim:ident; move_location
  | IDENT "intro"; prim:ident
  | IDENT "intro"
  | IDENT "assumption"
  | IDENT "exact"; constr:constr
  | IDENT "exact_no_check"; constr:constr
  | IDENT "vm_cast_no_check"; constr:constr
  | 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 tactic:constr_with_bindings SEP ","; in_hyp_as
  | IDENT "eapply"; LIST1 tactic:constr_with_bindings SEP ","; in_hyp_as
  | IDENT "elim"; tactic:constr_with_bindings; OPT eliminator
  | IDENT "eelim"; tactic:constr_with_bindings; OPT eliminator
  | IDENT "elimtype"; constr:constr
  | IDENT "case"; induction_clause_list
  | IDENT "ecase"; induction_clause_list
  | IDENT "casetype"; constr:constr
  | "fix"; prim:natural
  | "fix"; prim:ident; prim:natural; "with"; LIST1 fixdecl
  | "fix"; prim:ident; prim:natural
  | "cofix"; prim:ident; "with"; LIST1 cofixdecl
  | "cofix"; prim:ident
  | "cofix"
  | IDENT "set"; bindings_with_parameters; clause_dft_concl
  | IDENT "set"; constr:constr; as_name; clause_dft_concl
  | IDENT "remember"; constr:constr; as_name; eqn_ipat; clause_dft_all
  | IDENT "assert"; lpar_id_coloneq; "("; Prim.identref; ":=";
    constr:lconstr; ")"
  | IDENT "assert"; lpar_id_colon; "("; Prim.identref; ":"; constr:lconstr;
    ")"; by_tactic
  | IDENT "assert"; constr:constr; as_ipat; by_tactic
  | IDENT "pose"; IDENT "proof"; constr:lconstr; as_ipat
  | IDENT "pose"; bindings_with_parameters
  | IDENT "pose"; constr:constr; as_name
  | IDENT "cut"; constr:constr
  | IDENT "generalize"; IDENT "dependent"; constr:constr
  | IDENT "generalize"; constr:constr; LIST1 constr:constr
  | IDENT "generalize"; constr:constr; lookup_at_as_coma; occs; as_name;
    LIST0 [ ","; pattern_occ; as_name ]
  | IDENT "generalize"; constr:constr
  | IDENT "specialize"; OPT prim:natural; tactic:constr_with_bindings
  | IDENT "lapply"; constr:constr
  | IDENT "induction"; induction_clause_list
  | IDENT "einduction"; induction_clause_list
  | IDENT "double"; IDENT "induction"; tactic:quantified_hypothesis;
    tactic:quantified_hypothesis
  | IDENT "destruct"; induction_clause_list
  | IDENT "edestruct"; induction_clause_list
  | IDENT "decompose"; IDENT "record"; constr:constr
  | IDENT "decompose"; IDENT "sum"; constr:constr
  | IDENT "decompose"; "["; LIST1 smart_global; "]"; constr:constr
  | IDENT "trivial"; auto_using; hintbases
  | IDENT "info_trivial"; auto_using; hintbases
  | IDENT "auto"; OPT tactic:int_or_var; auto_using; hintbases
  | IDENT "info_auto"; OPT tactic:int_or_var; auto_using; hintbases
  | IDENT "debug"; IDENT "eauto"; OPT tactic:int_or_var;
    OPT tactic:int_or_var; tactic:auto_using; tactic:hintbases
  | IDENT "debug"; IDENT "trivial"; auto_using; hintbases
  | IDENT "debug"; IDENT "auto"; OPT tactic:int_or_var; auto_using; hintbases
  | IDENT "clear"; IDENT "dependent"; prim:var
  | IDENT "clear"; "-"; LIST1 id_or_meta
  | IDENT "clear"; LIST0 id_or_meta
  | IDENT "clearbody"; LIST1 id_or_meta
  | IDENT "move"; id_or_meta; move_location
  | IDENT "rename"; LIST1 rename SEP ","
  | IDENT "revert"; IDENT "dependent"; prim:var
  | IDENT "revert"; LIST1 id_or_meta
  | IDENT "left"; with_bindings
  | IDENT "eleft"; with_bindings
  | IDENT "right"; with_bindings
  | IDENT "eright"; with_bindings
  | IDENT "split"; with_bindings
  | IDENT "esplit"; with_bindings
  | "exists"; LIST1 opt_bindings SEP ","
  | IDENT "eexists"; LIST1 opt_bindings SEP ","
  | IDENT "constructor"; nat_or_var; with_bindings
  | IDENT "constructor"; OPT tactic:tactic
  | IDENT "econstructor"; nat_or_var; with_bindings
  | IDENT "econstructor"; OPT tactic:tactic
  | IDENT "reflexivity"
  | IDENT "symmetry"; clause_dft_concl
  | IDENT "transitivity"; constr:constr
  | IDENT "etransitivity"
  | IDENT "rewrite"; "*"; tactic:orient; tactic:open_constr; "in"; prim:var;
    "at"; tactic:occurrences; tactic:by_arg_tac
  | IDENT "rewrite"; "*"; tactic:orient; tactic:open_constr; "in"; prim:var;
    tactic:by_arg_tac
  | IDENT "rewrite"; "*"; tactic:orient; tactic:open_constr; "at";
    tactic:occurrences; "in"; prim:var; tactic:by_arg_tac
  | IDENT "rewrite"; "*"; tactic:orient; tactic:open_constr; "at";
    tactic:occurrences; tactic:by_arg_tac
  | IDENT "rewrite"; "*"; tactic:orient; tactic:open_constr;
    tactic:by_arg_tac
  | IDENT "rewrite"; LIST1 oriented_rewriter SEP ","; clause_dft_concl;
    opt_by_tactic
  | IDENT "erewrite"; LIST1 oriented_rewriter SEP ","; clause_dft_concl;
    opt_by_tactic
  | 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;
    with_inversion_names; OPT [ "with"; constr:constr ]
  | IDENT "simple"; IDENT "subst"
  | IDENT "simple"; IDENT "apply"; LIST1 tactic:constr_with_bindings SEP ",";
    in_hyp_as
  | IDENT "simple"; IDENT "eapply";
    LIST1 tactic:constr_with_bindings SEP ","; in_hyp_as
  | IDENT "simple"; IDENT "induction"; tactic:quantified_hypothesis
  | IDENT "simple"; IDENT "destruct"; tactic:quantified_hypothesis
  | IDENT "simple"; IDENT "inversion"; tactic:quantified_hypothesis;
    with_inversion_names; in_hyp_list
  | IDENT "inversion_clear"; tactic:quantified_hypothesis;
    with_inversion_names; in_hyp_list
  | IDENT "inversion"; tactic:quantified_hypothesis; "using"; constr:constr;
    in_hyp_list
  | IDENT "inversion"; tactic:quantified_hypothesis; with_inversion_names;
    in_hyp_list
  | IDENT "change"; conversion; clause_dft_concl
  | red_tactic; clause_dft_concl ] ]

<prompt>Coq < 6 || 0 < </prompt>Add Search Blacklist "Raw" "Proofs".

<prompt>Coq < 7 || 0 < </prompt>Set Search Output Name Only.

<prompt>Coq < 8 || 0 < </prompt>Redirect "/tmp/coq30429-9o" SearchPattern _.

<prompt>Coq < 9 || 0 < </prompt>Remove Search Blacklist "Raw" "Proofs".

<prompt>Coq < 10 || 0 < </prompt>Unset Search Output Name Only.

<prompt>Coq < 11 || 0 < </prompt>Timeout 1 Print LoadPath.
Logical Path:                 Physical path:
<>                            /home/jgross
<>                            /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/user-contrib
Coq                           /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins
Coq.firstorder                /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/firstorder
Coq.extraction                /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/extraction
Coq.ring                      /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/ring
Coq.subtac                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/subtac
Coq.quote                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/quote
Coq.setoid_ring               /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/setoid_ring
Coq.funind                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/funind
Coq.rtauto                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/rtauto
Coq.cc                        /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/cc
Coq.field                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/field
Coq.fourier                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/fourier
Coq.xml                       /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/xml
Coq.romega                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/romega
Coq.syntax                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/syntax
Coq.nsatz                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/nsatz
Coq.micromega                 /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/micromega
Coq.decl_mode                 /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/decl_mode
Coq.omega                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/omega
Coq                           /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/states
Coq.Init                      /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Init
Coq.Logic                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Logic
Coq.Bool                      /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Bool
Coq.Arith                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Arith
Coq.ZArith                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/ZArith
Coq.NArith                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/NArith
Coq.PArith                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/PArith
Coq.QArith                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/QArith
Coq.Numbers                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers
Coq.Numbers.Natural.SpecViaZ  /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Natural/SpecViaZ
Coq.Numbers.Natural.Binary    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Natural/Binary
Coq.Numbers.Natural.BigN      /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Natural/BigN
Coq.Numbers.Natural.Peano     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Natural/Peano
Coq.Numbers.Natural.Abstract  /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Natural/Abstract
Coq.Numbers.Natural           /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Natural
Coq.Numbers.NatInt            /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/NatInt
Coq.Numbers.Rational.SpecViaQ /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Rational/SpecViaQ
Coq.Numbers.Rational.BigQ     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Rational/BigQ
Coq.Numbers.Rational          /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Rational
Coq.Numbers.Integer.NatPairs  /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Integer/NatPairs
Coq.Numbers.Integer.SpecViaZ  /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Integer/SpecViaZ
Coq.Numbers.Integer.Binary    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Integer/Binary
Coq.Numbers.Integer.Abstract  /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Integer/Abstract
Coq.Numbers.Integer.BigZ      /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Integer/BigZ
Coq.Numbers.Integer           /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Integer
Coq.Numbers.Cyclic.DoubleCyclic 
                              /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Cyclic/DoubleCyclic
Coq.Numbers.Cyclic.Int31      /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Cyclic/Int31
Coq.Numbers.Cyclic.ZModulo    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Cyclic/ZModulo
Coq.Numbers.Cyclic.Abstract   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Cyclic/Abstract
Coq.Numbers.Cyclic            /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Cyclic
Coq.Relations                 /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Relations
Coq.Wellfounded               /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Wellfounded
Coq.Vectors                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Vectors
Coq.Lists                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Lists
Coq.Structures                /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Structures
Coq.Sets                      /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Sets
Coq.Setoids                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Setoids
Coq.Sorting                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Sorting
Coq.Strings                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Strings
Coq.Reals                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Reals
Coq.FSets                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/FSets
Coq.MSets                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/MSets
Coq.Program                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Program
Coq.Classes                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Classes
Coq.Unicode                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Unicode

<prompt>Coq < 12 || 0 < </prompt>Set Printing Depth 50 . 

<prompt>Coq < 13 || 0 < </prompt>Remove Search Blacklist "Private_" "_subproof".  Add Search Blacklist "Private_" "_subproof". 

<prompt>Coq < 14 || 0 < </prompt>
<prompt>Coq < 15 || 0 < </prompt>Set Printing Width 79.

<prompt>Coq < 16 || 0 < </prompt>Set Silent. 

<prompt>Coq < 17 || 0 < </prompt>Require Coq.Lists.List.

<prompt>Coq < 18 || 0 < </prompt>Module Operations.

<prompt>Coq < 19 || 0 < </prompt>Module Export List.

<prompt>Coq < 20 || 0 < </prompt>Axiom foobar : Set.

<prompt>Coq < 21 || 0 < </prompt>End List.

<prompt>Coq < 22 || 0 < </prompt>Axiom bazqux : Set.

<prompt>Coq < 23 || 0 < </prompt>Unset Silent. 

<prompt>Coq < 24 || 0 < </prompt>End Operations.
Module Operations is defined

<prompt>Coq < 25 || 0 < </prompt>Redirect "/tmp/coq30429LIv" Print Ltac Signatures.

<prompt>Coq < 26 || 0 < </prompt>Timeout 1 Print Grammar tactic.
Entry tactic_expr is
[ "5" RIGHTA
  [ tactic:binder_tactic ]
| "4" LEFTA
  [ SELF; ";"; "["; tactic_then_gen; "]"
  | SELF; ";"; tactic:binder_tactic
  | SELF; ";"; SELF ]
| "3" RIGHTA
  [ IDENT "try"; SELF
  | IDENT "do"; tactic:int_or_var; SELF
  | IDENT "timeout"; tactic:int_or_var; SELF
  | IDENT "repeat"; SELF
  | IDENT "progress"; SELF
  | IDENT "abstract"; NEXT; "using"; prim:ident
  | IDENT "abstract"; NEXT ]
| "2" RIGHTA
  [ SELF; "||"; tactic:binder_tactic
  | SELF; "||"; SELF ]
| "1" RIGHTA
  [ IDENT "first"; "["; LIST0 tactic:tactic_expr SEP "|"; "]"
  | IDENT "solve"; "["; LIST0 tactic:tactic_expr SEP "|"; "]"
  | IDENT "idtac"; LIST0 message_token
  | IDENT "fail"; [ tactic:int_or_var |  ]; LIST0 message_token
  | IDENT "external"; STRING; STRING; LIST1 tactic:tactic_arg
  | IDENT "constr"; ":"; METAIDENT
  | IDENT "constr"; ":"; constr:constr
  | IDENT "ipattern"; ":"; tactic:simple_intropattern
  | 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"
  | tactic:simple_tactic
  | may_eval_arg
  | prim:reference; LIST0 tactic:tactic_arg ]
| "0" LEFTA
  [ "("; SELF; ")"
  | tactic_atom ] ]
Entry 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 simple_tactic is
[ LEFTA
  [ 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 "poseq"; prim:ident; constr:constr
  | IDENT "fauto"; tactic:tactic
  | IDENT "fauto"
  | IDENT "finduction"; prim:ident; OPT prim:natural
  | IDENT "soft"; IDENT "functional"; IDENT "induction"; LIST1 constr:constr;
    tactic:fun_ind_using; tactic:with_names
  | IDENT "functional"; IDENT "induction"; LIST1 constr:constr;
    tactic:fun_ind_using; tactic:with_names
  | IDENT "functional"; IDENT "inversion"; tactic:quantified_hypothesis;
    OPT prim:reference
  | 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 "f_equal"
  | IDENT "congruence"; "with"; LIST1 constr:constr
  | IDENT "congruence"; prim:integer; "with"; LIST1 constr:constr
  | IDENT "congruence"; prim:integer
  | IDENT "congruence"
  | IDENT "stop"; IDENT "profiling"
  | IDENT "start"; IDENT "profiling"
  | IDENT "compare"; constr:constr; constr:constr
  | IDENT "decide"; IDENT "equality"
  | IDENT "decide"; constr:constr; "with"; constr:constr
  | IDENT "intuition"; tactic:tactic
  | IDENT "intuition"
  | IDENT "tauto"
  | IDENT "myapply"; constr:global; LIST0 constr:constr
  | IDENT "fold_matches"; constr:constr
  | IDENT "fold_match"; constr:constr
  | IDENT "implify"; prim:var
  | IDENT "setoid_transitivity"; constr:constr
  | IDENT "setoid_etransitivity"
  | IDENT "setoid_reflexivity"
  | IDENT "setoid_symmetry"; "in"; prim:var
  | IDENT "setoid_symmetry"
  | IDENT "rew"; tactic:orient; tactic:glob_constr_with_bindings; "in";
    prim:var; "at"; tactic:occurrences
  | IDENT "rew"; tactic:orient; tactic:glob_constr_with_bindings; "in";
    prim:var
  | IDENT "rew"; tactic:orient; tactic:glob_constr_with_bindings; "at";
    tactic:occurrences; "in"; prim:var
  | IDENT "rew"; tactic:orient; tactic:glob_constr_with_bindings; "at";
    tactic:occurrences
  | IDENT "rew"; tactic:orient; tactic:glob_constr_with_bindings
  | IDENT "setoid_rewrite"; tactic:orient; tactic:glob_constr_with_bindings;
    "at"; tactic:occurrences; "in"; prim:var
  | IDENT "setoid_rewrite"; tactic:orient; tactic:glob_constr_with_bindings;
    "at"; tactic:occurrences
  | IDENT "setoid_rewrite"; tactic:orient; tactic:glob_constr_with_bindings;
    "in"; prim:var; "at"; tactic:occurrences
  | IDENT "setoid_rewrite"; tactic:orient; tactic:glob_constr_with_bindings;
    "in"; prim:var
  | IDENT "setoid_rewrite"; tactic:orient; tactic:glob_constr_with_bindings
  | IDENT "substitute"; tactic:orient; tactic:glob_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 "autoapply"; constr:constr; "using"; prim:preident
  | IDENT "is_ground"; constr:constr
  | IDENT "not_evar"; constr:constr
  | IDENT "head_of_constr"; prim:ident; constr:constr
  | IDENT "typeclasses"; IDENT "eauto"; "with"; LIST1 prim:preident
  | IDENT "typeclasses"; IDENT "eauto"
  | IDENT "progress_evars"; tactic:tactic
  | IDENT "convert_concl_no_check"; constr:constr
  | IDENT "unify"; constr:constr; constr:constr; "with"; prim:preident
  | IDENT "unify"; constr:constr; constr:constr
  | IDENT "autounfoldify"; constr:constr
  | IDENT "autounfold_one"; tactic:hintbases; "in"; prim:var
  | IDENT "autounfold_one"; tactic:hintbases
  | IDENT "autounfold"; tactic:hintbases; tactic:in_arg_hyp
  | 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:open_constr; "]"; tactic:int_or_var
  | IDENT "eexact"; constr:constr
  | IDENT "eassumption"
  | IDENT "is_fix"; constr:constr
  | IDENT "is_var"; constr:constr
  | IDENT "has_evar"; constr:constr
  | IDENT "is_evar"; constr:constr
  | IDENT "constr_eq"; constr:constr; constr:constr
  | 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:integer; ":="; tactic:glob; ")";
    tactic:hloc
  | IDENT "instantiate"
  | IDENT "evar"; "("; prim:ident; ":"; constr:lconstr; ")"
  | IDENT "evar"; constr:constr
  | IDENT "subst"; LIST1 prim:var
  | IDENT "subst"
  | IDENT "refine"; tactic:casted_open_constr
  | IDENT "autorewrite"; "*"; "with"; LIST1 prim:preident; tactic:in_arg_hyp;
    "using"; tactic:tactic
  | IDENT "autorewrite"; "*"; "with"; LIST1 prim:preident; tactic:in_arg_hyp
  | IDENT "autorewrite"; "with"; LIST1 prim:preident; tactic:in_arg_hyp;
    "using"; tactic:tactic
  | IDENT "autorewrite"; "with"; LIST1 prim:preident; tactic:in_arg_hyp
  | IDENT "contradiction"; OPT tactic:constr_with_bindings
  | IDENT "absurd"; 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:quantified_hypothesis; "as";
    LIST0 tactic:simple_intropattern
  | IDENT "einjection"; tactic:quantified_hypothesis
  | IDENT "einjection"; tactic:constr_with_bindings; "as";
    LIST0 tactic:simple_intropattern
  | IDENT "einjection"; tactic:constr_with_bindings
  | IDENT "einjection"
  | IDENT "injection"; "as"; LIST0 tactic:simple_intropattern
  | IDENT "injection"; tactic:quantified_hypothesis; "as";
    LIST0 tactic:simple_intropattern
  | IDENT "injection"; tactic:quantified_hypothesis
  | IDENT "injection"; tactic:constr_with_bindings; "as";
    LIST0 tactic:simple_intropattern
  | IDENT "injection"; tactic:constr_with_bindings
  | IDENT "injection"
  | IDENT "ediscriminate"; tactic:quantified_hypothesis
  | IDENT "ediscriminate"; tactic:constr_with_bindings
  | IDENT "ediscriminate"
  | IDENT "discriminate"; tactic:quantified_hypothesis
  | IDENT "discriminate"; tactic:constr_with_bindings
  | IDENT "discriminate"
  | IDENT "esimplify_eq"; tactic:quantified_hypothesis
  | IDENT "esimplify_eq"; tactic:constr_with_bindings
  | IDENT "esimplify_eq"
  | IDENT "simplify_eq"; tactic:quantified_hypothesis
  | IDENT "simplify_eq"; tactic:constr_with_bindings
  | IDENT "simplify_eq"
  | IDENT "replace"; "<-"; tactic:open_constr; tactic:in_arg_hyp
  | IDENT "replace"; "->"; tactic:open_constr; tactic:in_arg_hyp
  | IDENT "replace"; tactic:open_constr; "with"; constr:constr; "at";
    tactic:occurrences; tactic:by_arg_tac
  | IDENT "replace"; tactic:open_constr; "with"; constr:constr;
    tactic:in_arg_hyp; tactic:by_arg_tac
  | IDENT "replace"; tactic:open_constr; tactic:in_arg_hyp
  | IDENT "admit"
  | IDENT "intros"; IDENT "until"; tactic:quantified_hypothesis
  | IDENT "intros"; intropatterns
  | IDENT "intro"; move_location
  | IDENT "intro"; prim:ident; move_location
  | IDENT "intro"; prim:ident
  | IDENT "intro"
  | IDENT "assumption"
  | IDENT "exact"; constr:constr
  | IDENT "exact_no_check"; constr:constr
  | IDENT "vm_cast_no_check"; constr:constr
  | 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 tactic:constr_with_bindings SEP ","; in_hyp_as
  | IDENT "eapply"; LIST1 tactic:constr_with_bindings SEP ","; in_hyp_as
  | IDENT "elim"; tactic:constr_with_bindings; OPT eliminator
  | IDENT "eelim"; tactic:constr_with_bindings; OPT eliminator
  | IDENT "elimtype"; constr:constr
  | IDENT "case"; induction_clause_list
  | IDENT "ecase"; induction_clause_list
  | IDENT "casetype"; constr:constr
  | "fix"; prim:natural
  | "fix"; prim:ident; prim:natural; "with"; LIST1 fixdecl
  | "fix"; prim:ident; prim:natural
  | "cofix"; prim:ident; "with"; LIST1 cofixdecl
  | "cofix"; prim:ident
  | "cofix"
  | IDENT "set"; bindings_with_parameters; clause_dft_concl
  | IDENT "set"; constr:constr; as_name; clause_dft_concl
  | IDENT "remember"; constr:constr; as_name; eqn_ipat; clause_dft_all
  | IDENT "assert"; lpar_id_coloneq; "("; Prim.identref; ":="; constr:lconstr;
    ")"
  | IDENT "assert"; lpar_id_colon; "("; Prim.identref; ":"; constr:lconstr;
    ")"; by_tactic
  | IDENT "assert"; constr:constr; as_ipat; by_tactic
  | IDENT "pose"; IDENT "proof"; constr:lconstr; as_ipat
  | IDENT "pose"; bindings_with_parameters
  | IDENT "pose"; constr:constr; as_name
  | IDENT "cut"; constr:constr
  | IDENT "generalize"; IDENT "dependent"; constr:constr
  | IDENT "generalize"; constr:constr; LIST1 constr:constr
  | IDENT "generalize"; constr:constr; lookup_at_as_coma; occs; as_name;
    LIST0 [ ","; pattern_occ; as_name ]
  | IDENT "generalize"; constr:constr
  | IDENT "specialize"; OPT prim:natural; tactic:constr_with_bindings
  | IDENT "lapply"; constr:constr
  | IDENT "induction"; induction_clause_list
  | IDENT "einduction"; induction_clause_list
  | IDENT "double"; IDENT "induction"; tactic:quantified_hypothesis;
    tactic:quantified_hypothesis
  | IDENT "destruct"; induction_clause_list
  | IDENT "edestruct"; induction_clause_list
  | IDENT "decompose"; IDENT "record"; constr:constr
  | IDENT "decompose"; IDENT "sum"; constr:constr
  | IDENT "decompose"; "["; LIST1 smart_global; "]"; constr:constr
  | IDENT "trivial"; auto_using; hintbases
  | IDENT "info_trivial"; auto_using; hintbases
  | IDENT "auto"; OPT tactic:int_or_var; auto_using; hintbases
  | IDENT "info_auto"; OPT tactic:int_or_var; auto_using; hintbases
  | IDENT "debug"; IDENT "eauto"; OPT tactic:int_or_var;
    OPT tactic:int_or_var; tactic:auto_using; tactic:hintbases
  | IDENT "debug"; IDENT "trivial"; auto_using; hintbases
  | IDENT "debug"; IDENT "auto"; OPT tactic:int_or_var; auto_using; hintbases
  | IDENT "clear"; IDENT "dependent"; prim:var
  | IDENT "clear"; "-"; LIST1 id_or_meta
  | IDENT "clear"; LIST0 id_or_meta
  | IDENT "clearbody"; LIST1 id_or_meta
  | IDENT "move"; id_or_meta; move_location
  | IDENT "rename"; LIST1 rename SEP ","
  | IDENT "revert"; IDENT "dependent"; prim:var
  | IDENT "revert"; LIST1 id_or_meta
  | IDENT "left"; with_bindings
  | IDENT "eleft"; with_bindings
  | IDENT "right"; with_bindings
  | IDENT "eright"; with_bindings
  | IDENT "split"; with_bindings
  | IDENT "esplit"; with_bindings
  | "exists"; LIST1 opt_bindings SEP ","
  | IDENT "eexists"; LIST1 opt_bindings SEP ","
  | IDENT "constructor"; nat_or_var; with_bindings
  | IDENT "constructor"; OPT tactic:tactic
  | IDENT "econstructor"; nat_or_var; with_bindings
  | IDENT "econstructor"; OPT tactic:tactic
  | IDENT "reflexivity"
  | IDENT "symmetry"; clause_dft_concl
  | IDENT "transitivity"; constr:constr
  | IDENT "etransitivity"
  | IDENT "rewrite"; "*"; tactic:orient; tactic:open_constr; "in"; prim:var;
    "at"; tactic:occurrences; tactic:by_arg_tac
  | IDENT "rewrite"; "*"; tactic:orient; tactic:open_constr; "in"; prim:var;
    tactic:by_arg_tac
  | IDENT "rewrite"; "*"; tactic:orient; tactic:open_constr; "at";
    tactic:occurrences; "in"; prim:var; tactic:by_arg_tac
  | IDENT "rewrite"; "*"; tactic:orient; tactic:open_constr; "at";
    tactic:occurrences; tactic:by_arg_tac
  | IDENT "rewrite"; "*"; tactic:orient; tactic:open_constr; tactic:by_arg_tac
  | IDENT "rewrite"; LIST1 oriented_rewriter SEP ","; clause_dft_concl;
    opt_by_tactic
  | IDENT "erewrite"; LIST1 oriented_rewriter SEP ","; clause_dft_concl;
    opt_by_tactic
  | 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;
    with_inversion_names; OPT [ "with"; constr:constr ]
  | IDENT "simple"; IDENT "subst"
  | IDENT "simple"; IDENT "apply"; LIST1 tactic:constr_with_bindings SEP ",";
    in_hyp_as
  | IDENT "simple"; IDENT "eapply"; LIST1 tactic:constr_with_bindings SEP ",";
    in_hyp_as
  | IDENT "simple"; IDENT "induction"; tactic:quantified_hypothesis
  | IDENT "simple"; IDENT "destruct"; tactic:quantified_hypothesis
  | IDENT "simple"; IDENT "inversion"; tactic:quantified_hypothesis;
    with_inversion_names; in_hyp_list
  | IDENT "inversion_clear"; tactic:quantified_hypothesis;
    with_inversion_names; in_hyp_list
  | IDENT "inversion"; tactic:quantified_hypothesis; "using"; constr:constr;
    in_hyp_list
  | IDENT "inversion"; tactic:quantified_hypothesis; with_inversion_names;
    in_hyp_list
  | IDENT "change"; conversion; clause_dft_concl
  | red_tactic; clause_dft_concl ] ]

<prompt>Coq < 27 || 0 < </prompt>Add Search Blacklist "Raw" "Proofs".

<prompt>Coq < 28 || 0 < </prompt>Set Search Output Name Only.

<prompt>Coq < 29 || 0 < </prompt>Redirect "/tmp/coq30429YS1" SearchPattern _.

<prompt>Coq < 30 || 0 < </prompt>Remove Search Blacklist "Raw" "Proofs".

<prompt>Coq < 31 || 0 < </prompt>Unset Search Output Name Only.

<prompt>Coq < 32 || 0 < </prompt>Timeout 1 Print LoadPath.
Logical Path:                 Physical path:
<>                            /home/jgross
<>                            /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/user-contrib
Coq                           /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins
Coq.firstorder                /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/firstorder
Coq.extraction                /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/extraction
Coq.ring                      /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/ring
Coq.subtac                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/subtac
Coq.quote                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/quote
Coq.setoid_ring               /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/setoid_ring
Coq.funind                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/funind
Coq.rtauto                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/rtauto
Coq.cc                        /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/cc
Coq.field                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/field
Coq.fourier                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/fourier
Coq.xml                       /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/xml
Coq.romega                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/romega
Coq.syntax                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/syntax
Coq.nsatz                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/nsatz
Coq.micromega                 /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/micromega
Coq.decl_mode                 /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/decl_mode
Coq.omega                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/plugins/omega
Coq                           /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/states
Coq.Init                      /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Init
Coq.Logic                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Logic
Coq.Bool                      /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Bool
Coq.Arith                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Arith
Coq.ZArith                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/ZArith
Coq.NArith                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/NArith
Coq.PArith                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/PArith
Coq.QArith                    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/QArith
Coq.Numbers                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers
Coq.Numbers.Natural.SpecViaZ  /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Natural/SpecViaZ
Coq.Numbers.Natural.Binary    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Natural/Binary
Coq.Numbers.Natural.BigN      /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Natural/BigN
Coq.Numbers.Natural.Peano     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Natural/Peano
Coq.Numbers.Natural.Abstract  /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Natural/Abstract
Coq.Numbers.Natural           /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Natural
Coq.Numbers.NatInt            /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/NatInt
Coq.Numbers.Rational.SpecViaQ /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Rational/SpecViaQ
Coq.Numbers.Rational.BigQ     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Rational/BigQ
Coq.Numbers.Rational          /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Rational
Coq.Numbers.Integer.NatPairs  /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Integer/NatPairs
Coq.Numbers.Integer.SpecViaZ  /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Integer/SpecViaZ
Coq.Numbers.Integer.Binary    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Integer/Binary
Coq.Numbers.Integer.Abstract  /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Integer/Abstract
Coq.Numbers.Integer.BigZ      /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Integer/BigZ
Coq.Numbers.Integer           /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Integer
Coq.Numbers.Cyclic.DoubleCyclic 
                              /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Cyclic/DoubleCyclic
Coq.Numbers.Cyclic.Int31      /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Cyclic/Int31
Coq.Numbers.Cyclic.ZModulo    /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Cyclic/ZModulo
Coq.Numbers.Cyclic.Abstract   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Cyclic/Abstract
Coq.Numbers.Cyclic            /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Numbers/Cyclic
Coq.Relations                 /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Relations
Coq.Wellfounded               /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Wellfounded
Coq.Vectors                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Vectors
Coq.Lists                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Lists
Coq.Structures                /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Structures
Coq.Sets                      /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Sets
Coq.Setoids                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Setoids
Coq.Sorting                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Sorting
Coq.Strings                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Strings
Coq.Reals                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Reals
Coq.FSets                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/FSets
Coq.MSets                     /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/MSets
Coq.Program                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Program
Coq.Classes                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Classes
Coq.Unicode                   /home/jgross/.local64/coq/coq-8.4pl6/lib/coq/theories/Unicode

<prompt>Coq < 33 || 0 < </prompt>
cpitclaudel commented 8 years ago

Ah. That's the SearchAbout vs SearchPattern thing. Did you add

(setq company-coq-extra-symbols-cmd "SearchAbout -\"____\"")

to your .emacs?

cpitclaudel commented 8 years ago

The issue is that SearchPattern and SearchAbout don't find the same things in 8.4, but the former subsumes the latter in 8.5.

cpitclaudel commented 8 years ago

Here's an example:

diff -u -Z /scratch/search-pattern /scratch/search-about
--- /scratch/search-pattern 2016-03-02 14:09:23.754020568 -0700
+++ /scratch/search-about   2016-03-02 14:09:30.442020448 -0700
@@ -1,4 +1,3 @@
-Acc
 Acc_ind
 Acc_intro
 Acc_inv
@@ -105,7 +104,6 @@
 Bool.orb_true_intro
 Bool.orb_true_l
 Bool.orb_true_r
-Bool.reflect
 Bool.reflect_dec
 Bool.reflect_iff
 Bool.reflect_ind
@@ -125,7 +123,6 @@
 Bool.xorb_nilpotent
 Bool.xorb_true_l
 Bool.xorb_true_r
-BoolSpec
 BoolSpecF
 BoolSpecT
 BoolSpec_ind
@@ -144,14 +141,11 @@
 CompSpec
 CompSpec2Type
 CompSpecT
-CompareSpec
 CompareSpec2Type
-CompareSpecT
 CompareSpecT_ind
 CompareSpecT_rec
 CompareSpecT_rect
 CompareSpec_ind
-Empty_set
 Empty_set_ind
 Empty_set_rec
 Empty_set_rect
@@ -174,7 +168,6 @@
 Equivalence.respecting_equiv_obligation_2
 Equivalence.respecting_equiv_obligation_3
 Exc
-False
 False_ind
 False_rec
 False_rect
@@ -226,7 +219,6 @@
 Le.le_pred_n
 Le.le_refl
 Le.le_trans
-List.Exists
 List.Exists_cons
 List.Exists_cons_hd
 List.Exists_cons_tl
@@ -235,8 +227,6 @@
 List.Exists_nil
 List.FOP_cons
 List.FOP_nil
-List.Forall
-List.Forall2
 List.Forall2_app
 List.Forall2_app_inv_l
 List.Forall2_app_inv_r
@@ -244,7 +234,6 @@
 List.Forall2_ind
 List.Forall2_nil
 List.Forall2_refl
-List.ForallOrdPairs
 List.ForallOrdPairs_ForallPairs
 List.ForallOrdPairs_In
 List.ForallOrdPairs_ind
@@ -258,7 +247,6 @@
 List.Forall_nil
 List.Forall_rect
 List.In
-List.NoDup
 List.NoDup_cons
 List.NoDup_ind
 List.NoDup_nil
@@ -456,11 +444,9 @@
 Morphisms.Normalizes
 Morphisms.PER_morphism
 Morphisms.PER_morphism_obligation_1
-Morphisms.Params
 Morphisms.Params_ind
 Morphisms.Params_rec
 Morphisms.Params_rect
-Morphisms.PartialApplication
 Morphisms.PartialApplication_ind
 Morphisms.PartialApplication_rec
 Morphisms.PartialApplication_rect
@@ -471,7 +457,6 @@
 Morphisms.Reflexive_partial_app_morphism
 Morphisms.StrictOrder_PartialOrder
 Morphisms.StrictOrder_PreOrder
-Morphisms.apply_subrelation
 Morphisms.complement_proper
 Morphisms.complement_proper_obligation_1
 Morphisms.compose_proper
@@ -492,7 +477,6 @@
 Morphisms.inverse_arrow
 Morphisms.inverse_atom
 Morphisms.inverse_respectful
-Morphisms.normalization_done
 Morphisms.normalizes
 Morphisms.per_partial_app_morphism
 Morphisms.per_partial_app_morphism_obligation_1
@@ -570,6 +554,8 @@
 None
 O
 O_S
+Operations.List.foobar
+Operations.bazqux
 Plus.le_plus_l
 Plus.le_plus_r
 Plus.le_plus_trans
@@ -607,7 +593,6 @@
 RelationClasses.Build_PreOrder
 RelationClasses.Build_RewriteRelation
 RelationClasses.Build_StrictOrder
-RelationClasses.Equivalence
 RelationClasses.Equivalence_PER
 RelationClasses.Equivalence_Reflexive
 RelationClasses.Equivalence_Symmetric
@@ -616,7 +601,6 @@
 RelationClasses.Equivalence_rec
 RelationClasses.Equivalence_rect
 RelationClasses.Irreflexive
-RelationClasses.PER
 RelationClasses.PER_Symmetric
 RelationClasses.PER_Transitive
 RelationClasses.PER_ind
@@ -624,7 +608,6 @@
 RelationClasses.PER_rect
 RelationClasses.PartialOrder
 RelationClasses.PartialOrder_inverse
-RelationClasses.PreOrder
 RelationClasses.PreOrder_Reflexive
 RelationClasses.PreOrder_Transitive
 RelationClasses.PreOrder_ind
@@ -633,14 +616,12 @@
 RelationClasses.PreOrder_rect
 RelationClasses.Reflexive
 RelationClasses.Reflexive_complement_Irreflexive
-RelationClasses.RewriteRelation
 RelationClasses.RewriteRelation_ind
 RelationClasses.RewriteRelation_instance_0
 RelationClasses.RewriteRelation_instance_1
 RelationClasses.RewriteRelation_instance_2
 RelationClasses.RewriteRelation_rec
 RelationClasses.RewriteRelation_rect
-RelationClasses.StrictOrder
 RelationClasses.StrictOrder_Asymmetric
 RelationClasses.StrictOrder_Irreflexive
 RelationClasses.StrictOrder_Transitive
@@ -650,7 +631,6 @@
 RelationClasses.StrictOrder_rect
 RelationClasses.Symmetric
 RelationClasses.Tcons
-RelationClasses.Tlist
 RelationClasses.Tlist_ind
 RelationClasses.Tlist_rec
 RelationClasses.Tlist_rect
@@ -722,7 +702,6 @@
 Relation_Definitions.Build_equivalence
 Relation_Definitions.Build_order
 Relation_Definitions.Build_preorder
-Relation_Definitions.PER
 Relation_Definitions.PER_ind
 Relation_Definitions.PER_rec
 Relation_Definitions.PER_rect
@@ -732,7 +711,6 @@
 Relation_Definitions.equiv_refl
 Relation_Definitions.equiv_sym
 Relation_Definitions.equiv_trans
-Relation_Definitions.equivalence
 Relation_Definitions.equivalence_ind
 Relation_Definitions.equivalence_rec
 Relation_Definitions.equivalence_rect
@@ -740,7 +718,6 @@
 Relation_Definitions.ord_antisym
 Relation_Definitions.ord_refl
 Relation_Definitions.ord_trans
-Relation_Definitions.order
 Relation_Definitions.order_ind
 Relation_Definitions.order_rec
 Relation_Definitions.order_rect
@@ -748,7 +725,6 @@
 Relation_Definitions.per_trans
 Relation_Definitions.preord_refl
 Relation_Definitions.preord_trans
-Relation_Definitions.preorder
 Relation_Definitions.preorder_ind
 Relation_Definitions.preorder_rec
 Relation_Definitions.preorder_rect
@@ -765,7 +741,6 @@
 Setoid.Setoid_Theory
 Setoid.gen_st
 SetoidTactics.Build_DefaultRelation
-SetoidTactics.DefaultRelation
 SetoidTactics.DefaultRelation_ind
 SetoidTactics.DefaultRelation_rec
 SetoidTactics.DefaultRelation_rect
@@ -774,14 +749,12 @@
 Some
 Tactics.fix_proto
 Tactics.obligation
-True
 True_ind
 True_rec
 True_rect
 absurd
 absurd_set
 all
-and
 and_assoc
 and_cancel_l
 and_cancel_r
@@ -795,12 +768,10 @@
 andb_prop
 andb_true_intro
 app
-bool
 bool_choice
 bool_ind
 bool_rec
 bool_rect
-comparison
 comparison_ind
 comparison_rec
 comparison_rect
@@ -809,7 +780,6 @@
 decide_left
 decide_right
 dependent_choice
-eq
 eq_S
 eq_add_S
 eq_ind
@@ -822,7 +792,6 @@
 eq_stepl
 eq_sym
 eq_trans
-eq_true
 eq_true_ind
 eq_true_ind_r
 eq_true_rec
@@ -830,8 +799,6 @@
 eq_true_rect
 eq_true_rect_r
 error
-ex
-ex2
 ex2_ind
 ex_ind
 ex_intro
@@ -855,7 +822,6 @@
 gen
 gt
 id
-identity
 identity_congr
 identity_ind
 identity_ind_r
@@ -874,7 +840,6 @@
 iff_to_and
 iff_trans
 implb
-inhabited
 inhabited_ind
 inhabits
 injective_projections
@@ -885,7 +850,6 @@
 inst
 is_eq_true
 is_true
-le
 le_S
 le_S_n
 le_ind
@@ -893,7 +857,6 @@
 le_pred
 left
 length
-list
 list_ind
 list_rec
 list_rect
@@ -909,7 +872,6 @@
 mult_n_O
 mult_n_Sm
 n_Sn
-nat
 nat_case
 nat_double_ind
 nat_ind
@@ -927,12 +889,10 @@
 not_eq_S
 not_eq_sym
 not_identity_sym
-option
 option_ind
 option_map
 option_rec
 option_rect
-or
 or_assoc
 or_cancel_l
 or_cancel_r
@@ -951,7 +911,6 @@
 plus_n_Sm
 pred
 pred_Sn
-prod
 prod_curry
 prod_ind
 prod_rec
@@ -964,13 +923,9 @@
 projT1
 projT2
 right
-sig
-sig2
 sig2_ind
 sig2_rec
 sig2_rect
-sigT
-sigT2
 sigT2_ind
 sigT2_rec
 sigT2_rect
@@ -984,15 +939,12 @@
 sig_rect
 snd
 subrelation
-sum
 sum_ind
 sum_rec
 sum_rect
-sumbool
 sumbool_ind
 sumbool_rec
 sumbool_rect
-sumor
 sumor_ind
 sumor_rec
 sumor_rect
@@ -1002,7 +954,6 @@
 unique
 unique_existence
 uniqueness
-unit
 unit_ind
 unit_rec
 unit_rect

Diff finished.  Wed Mar  2 14:09:44 2016
JasonGross commented 8 years ago

Adding (setq company-coq-extra-symbols-cmd "SearchAbout -\"____\"") fixed it. Thanks! Are there any downsides to doing this? Should this be the default for 8.4?

cpitclaudel commented 8 years ago

Great :) I'll add it to the docs (I'm not sure it's worth special-casing 8.4) The main downside is that it makes every symbols reload twice as slow. This is perceptible for projects with many imported modules.