auto-complete-coq.el

(require 'auto-complete)

(defvar ac-coq-sources
  '(ac-source-coq-tactics
    ac-source-coq-command
    ac-source-coq-keyword))

(ac-define-dictionary-source
 ac-source-coq-keyword
 '("as"
   "at"
   "cofix"
   "else"
   "end"
   "exists"
   "exists2"
   "fix"
   "for"
   "forall"
   "fun"
   "if"
   "in"
   "let"
   "match"
   "mod"
   "return"
   "then"
   "using"
   "where"
   "with"))

(ac-define-dictionary-source
 ac-source-coq-command
 '("About"
   "Add Field"
   "Add Legacy Abstract Ring"
   "Add Legacy Abstract Semi Ring"
   "Add Legacy Field"
   "Add Legacy Ring"
   "Add Legacy Semi Ring"
   "Add LoadPath"
   "Add ML Path"
   "Add Morphism"
   "Add Parametric Morphism"
   "Add Parametric Relation"
   "Add Printing If"
   "Add Printing Let"
   "Add Rec LoadPath"
   "Add Rec ML Path"
   "Add Relation"
   "Add Ring"
   "Add Setoid"
   "Admit Obligations"
   "Admitted"
   "Arguments Scope"
   "Axiom"
   "Back"
   "BackTo"
   "Backtrack"
   "Bind Scope"
   "Canonical Structure"
   "Cd"
   "Check"
   "Class"
   "Close Scope"
   "Coercion"
   "CoFixpoint"
   "CoInductive"
   "Combined Scheme"
   "Conjecture"
   "Corollary"
   "CreateHintDb"
   "Declare Implicit Tactic"
   "Declare Left Step"
   "Declare ML Module"
   "Declare Right Step"
   "Defined"
   "Definition"
   "Delimit Scope"
   "Derive Dependent Inversion"
   "Derive Dependent Inversion_clear"
   "Derive Inversion"
   "Derive Inversion_clear"
   "Drop"
   "End"
   "Eval"
   "Example"
   "Existential"
   "Existing Instance"
   "Export"
   "Extract Constant"
   "Extract Inductive"
   "Extraction"
   "Extraction Blaclist"
   "Extraction Inline"
   "Extraction Language"
   "Extraction Module"
   "Extraction NoInline"
   "Fact"
   "Fixpoint"
   "Focus"
   "Function"
   "Functional Scheme"
   "Global Implicit Arguments"
   "Goal"
   "Guarded"
   "Hint"
   "Hint Constructors"
   "Hint Extern"
   "Hint Immediate"
   "Hint Opaque"
   "Hint Resolve"
   "Hint Rewrite"
   "Hint Transparent"
   "Hint Unfold"
   "Hypotheses"
   "Hypothesis"
   "Identity Coercion"
   "Implicit Arguments"
   "Implicit Types"
   "Import"
   "Include"
   "Inductive"
   "Infix"
   "Inline"
   "Inspect"
   "Instance"
   "Lemma"
   "Let"
   "Load"
   "Load Verbose"
   "Local Coercion"
   "Local Implicit Arguments"
   "Local Strategy"
   "Locate"
   "Locate Library"
   "Locate Module"
   "Ltac"
   "Module"
   "Module Type"
   "Mutual Inductive"
   "Next Obligation"
   "Notation"
   "Obligation"
   "Obligation Tactic"
   "Obligations"
   "Opaque"
   "Open Scope"
   "Parameter"
   "Parameters"
   "Preterm"
   "Print"
   "Print All"
   "Print Assumptions"
   "Print Canonical Projections"
   "Print Classes"
   "Print Coercion Paths"
   "Print Coercions"
   "Print Extraction Inline"
   "Print Grammar constr"
   "Print Grammar pattern"
   "Print Graph"
   "Print Hint"
   "Print HintDb"
   "Print Implicit"
   "Print Libraries"
   "Print LoadPath"
   "Print Ltac"
   "Print ML Modules"
   "Print ML Path"
   "Print Module"
   "Print Module Type"
   "Print Section"
   "Print Table Printing If"
   "Print Table Printing Let"
   "Print Term"
   "Print Universes"
   "Print XML"
   "Program Definition"
   "Program Fixpoint"
   "Program Instance"
   "Program Lemma"
   "Proof"
   "Proof with"
   "Proposition"
   "Pwd"
   "Qed"
   "Quit"
   "Record"
   "Recursive Extraction"
   "Recursive Extraction Module"
   "Remark"
   "Remove LoadPath"
   "Remove Printing If"
   "Remove Printing Let"
   "Require"
   "Require Import"
   "Require Export"
   "ReservedNotation"
   "Reset"
   "Reset Extraction Inline"
   "Reset Initial"
   "Restart"
   "Restore State"
   "Resume"
   "Save"
   "Scheme"
   "Scheme Equality"
   "Search"
   "SearchAbout"
   "SearchPattern"
   "SearchRewrite"
   "Section"
   "Set Contextual Implicit"
   "Set Elimination Schemes"
   "Set Equality Scheme"
   "Set Extraction AutoInline"
   "Set Extraction Optimize"
   "Set Firstorder Depth"
   "Set Hyps Limit"
   "Set Implicit Arguments"
   "Set Ltac Debug"
   "Set Maximal Implicit Insertion"
   "Set Printing All"
   "Set Printing Coercion"
   "Set Printing Coercions"
   "Set Printing Depth"
   "Set Printing Implicit"
   "Set Printing Implicit Defensive"
   "Set Printing Matching"
   "Set Printing Notations"
   "Set Printing Synth"
   "Set Printing Universes"
   "Set Printing Width"
   "Set Printing Wildcard"
   "Set Reversible Pattern Implicit"
   "Set Silent"
   "Set Strict Implicit"
   "Set Strongly Strict Implicit"
   "Set Transparent Obligations"
   "Set Undo"
   "Set Virtual Machine"
   "Set Whelp Getter"
   "Set Whelp Server"
   "Show"
   "Show Conjectures"
   "Show Existentials"
   "Show Implicits"
   "Show Intro"
   "Show Intros"
   "Show Proof"
   "Show Script"
   "Show Tree"
   "Show XML Proof"
   "Solve Obligations"
   "Strategy"
   "Structure"
   "SubClass"
   "Suspend"
   "setoid_reflexivity"
   "setoid_replace"
   "setoid_rewrite"
   "setoid_symmetry"
   "setoid_transitivity"
   "Tactic Definition"
   "Test Ltac Debug"
   "Test Printing Depth"
   "Test Printing If for"
   "Test Printing Let for"
   "Test Printing Matching"
   "Test Printing Synth"
   "Test Printing Width"
   "Test Printing Wildcard"
   "Test Virtual Machine"
   "Test Whelp Server"
   "Theorem"
   "Time"
   "Transparent"
   "Typeclasses eauto"
   "Typeclasses Opaque"
   "Typeclasses Transparent"
   "Undo"
   "Unfocus"
   "Unset Contextual Implicit"
   "Unset Extraction AutoInline"
   "Unset Extraction Optimize"
   "Unset Hyps Limit"
   "Unset Implicit Arguments"
   "Unset Ltac Debug"
   "Unset Maximal Implicit Insertion"
   "Unset Printing All"
   "Unset Printing Coercion"
   "Unset Printing Coercions"
   "Unset Printing Depth"
   "Unset Printing Implicit"
   "Unset Printing Implicit Defensive"
   "Unset Printing Matching"
   "Unset Printing Notations"
   "Unset Printing Synth"
   "Unset Printing Universes"
   "Unset Printing Width"
   "Unset Printing Wildcard"
   "Unset Reversible Pattern Implicit"
   "Unset Silent"
   "Unset Strict Implicit"
   "Unset Strongly Strict Implicit"
   "Unset Undo"
   "Unset Virtual Machine"
   "Variable"
   "Variables"
   "Whelp Elim"
   "Whelp Hint"
   "Whelp Instance"
   "Whelp Locate"
   "Whelp Match"
   "Write State"))

(ac-define-dictionary-source
 ac-source-coq-tactics
 '("abstract"
   "absurd"
   "admit"
   "apply"
   "assert"
   "assumption"
   "auto"
   "autorewrite"
   "case"
   "case_eq"
   "cbv"
   "change"
   "classical_left"
   "classical_right"
   "clear"
   "clearbody"
   "cofix"
   "compare"
   "compute"
   "congruence"
   "constructor"
   "contradict"
   "contradiction"
   "cut"
   "cutrewrite"
   "decide"
   "decompose"
   "dependent"
   "destruct"
   "discriminate"
   "discrR"
   "do"
   "double"
   "eapply"
   "eassumption"
   "eauto"
   "ecase"
   "econstructor"
   "edestruct"
   "ediscriminate"
   "eelim"
   "eexact"
   "eexists"
   "einduction"
   "einjection"
   "eleft"
   "elim"
   "elimtype"
   "erewrite"
   "eright"
   "esimplify_eq"
   "esplit"
   "evar"
   "exact"
   "exists"
   "f_equal"
   "fail"
   "field"
   "field_simplify"
   "field_simplify_eq"
   "first"
   "firstorder"
   "fix"
   "fold"
   "fourier"
   "functional"
   "gappa"
   "generalize"
   "hnf"
   "idtac"
   "induction"
   "info"
   "injection"
   "instantiate"
   "intro"
   "intros"
   "intuition"
   "inversion"
   "inversion_clear"
   "inversion_cleardots"
   "lapply"
   "lazy"
   "left"
   "legacy"
   "move"
   "omega"
   "pattern"
   "pose"
   "progress"
   "quote"
   "red"
   "refine"
   "reflexivity"
   "remember"
   "rename"
   "repeat"
   "replace"
   "revert"
   "rewrite"
   "right"
   "ring"
   "ring_simplify"
   "rtauto"
   "set"
   "setoid_replace"
   "simpl"
   "simple"
   "simplify_eq"
   "solve"
   "specialize"
   "split"
   "split_Rabs"
   "split_Rmult"
   "stepl"
   "stepr"
   "subst"
   "symmetry"
   "tauto"
   "transitivity"
   "trivial"
   "try"
   "unfold"
   "vm_compute"))

(defun ac-coq-setup ()
  (setq ac-sources (append ac-coq-sources ac-sources)))

(defun ac-coq-init ()
  (add-hook 'coq-mode-hook 'ac-coq-setup))

(provide 'auto-complete-coq)