search

cpitclaudel / company-coq

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

Missing completions #74

Open JasonGross opened 8 years ago

JasonGross commented 8 years ago

I'm going to make this issue and add things to it as I find them missing. Do you want to leave this issue open (or something) so there's a single place to report missing completions?

cpitclaudel commented 8 years ago

:+1:

cpitclaudel commented 8 years ago

Is Set Keyed Unification documented?

JasonGross commented 8 years ago

If it's not, that's a bug, and it should be. (At the very least, it's in the commit message for the feature.)

cpitclaudel commented 8 years ago

I'll have to wait for it to be in the manual; completions are taken from there.

JasonGross commented 8 years ago

Bug #4551

cpitclaudel commented 8 years ago

Is Set Asymmetric Patterns another undocumented option?

JasonGross commented 8 years ago

The following options exist in the source code (grepping for optkey), but not in the tactics index:

Asymmetric Patterns
Atomic Load
Bullet Behavior
Compat Notations
Congruence Depth
Congruence Verbose
Debug Eauto
Debug RAKAM
Debug Tactic Unification
Debug Unification
Default Clearing Used Hypotheses
Default Proof Mode
Dependent Propositions Elimination
Discriminate Introduction
Dump Bytecode
Equality Scheme
Extraction File Comment
Extraction Flag
Extraction name
Functional Induction Rewrite Dependent
Function_debug
Function_raw_tcc
Info Eauto
Injection L2R Pattern Order
Injection On Proofs
Inline Level
Kernel Term Sharing
Keyed Unification
Omega Action
Omega OldStyle
Omega System
Program Mode
Proof Using Clear Unused
Record Elimination Schemes
Rewriting Schemes
Rtauto Check
Rtauto Pruning
Rtauto Verbose
Short Module Printing
SimplIsCbn
Stable Omega
Standard Proposition Elimination Names
Strict Proofs
Tactic Evars Pattern Unification
Tactic Pattern Unification
Typeclasses Debug
Typeclasses Dependency Order
Typeclasses Depth
Typeclasses Modulo Eta
Typeclasses Strict Resolution
Typeclasses Unique Instances
Typeclasses Unique Solutions
Typeclass Resolution After Apply
Typeclass Resolution For Conversion
Undo
Verbose Compat Notations
JasonGross commented 8 years ago

Note that Scheme Minimality and Scheme ident := Equality ... are not currently literally documented as variants. If it'd be helpful, I can open a bug report or submit a PR or something, to the Coq documentation.

cpitclaudel commented 8 years ago

I'm inclined to suspend these changes until we get the new manual format; things should be much simpler there.