; Generated on Thu Dec 17 16:14:05 2015

(defvar easycrypt-bytac-keywords '(
  "exact"
  "assumption"
  "smt"
  "by"
  "reflexivity"
  "done"
))

(defvar easycrypt-dangerous-keywords '(
  "admit"
  "admitted"
))

(defvar easycrypt-global-keywords '(
  "axiom"
  "axiomatized"
  "lemma"
  "realize"
  "proof"
  "qed"
  "abort"
  "goal"
  "end"
  "import"
  "export"
  "include"
  "local"
  "declare"
  "hint"
  "nosmt"
  "module"
  "of"
  "const"
  "op"
  "pred"
  "notation"
  "abbrev"
  "require"
  "theory"
  "abstract"
  "section"
  "type"
  "class"
  "instance"
  "print"
  "search"
  "as"
  "Pr"
  "clone"
  "with"
  "rename"
  "prover"
  "timeout"
  "why3"
  "dump"
  "remove"
  "Top"
  "Self"
))

(defvar easycrypt-internal-keywords '(
  "time"
  "undo"
  "debug"
  "pragma"
))

(defvar easycrypt-prog-keywords '(
  "forall"
  "exists"
  "fun"
  "glob"
  "let"
  "in"
  "var"
  "proc"
  "if"
  "then"
  "else"
  "elif"
  "while"
  "assert"
  "return"
  "res"
  "equiv"
  "hoare"
  "phoare"
  "islossless"
))

(defvar easycrypt-tactic-keywords '(
  "beta"
  "iota"
  "zeta"
  "eta"
  "logic"
  "delta"
  "simplify"
  "congr"
  "change"
  "split"
  "left"
  "right"
  "case"
  "pose"
  "cut"
  "have"
  "suff"
  "elim"
  "clear"
  "apply"
  "rewrite"
  "rwnormal"
  "subst"
  "progress"
  "trivial"
  "auto"
  "idtac"
  "move"
  "modpath"
  "field"
  "fieldeq"
  "ring"
  "ringeq"
  "algebra"
  "transitivity"
  "symmetry"
  "seq"
  "wp"
  "sp"
  "sim"
  "skip"
  "call"
  "rcondt"
  "rcondf"
  "swap"
  "cfold"
  "rnd"
  "pr_bounded"
  "bypr"
  "byphoare"
  "byequiv"
  "fel"
  "conseq"
  "exfalso"
  "inline"
  "alias"
  "fission"
  "fusion"
  "unroll"
  "splitwhile"
  "kill"
  "eager"
))

(defvar easycrypt-tactical-keywords '(
  "try"
  "first"
  "last"
  "do"
  "strict"
  "expect"
))

(provide 'easycrypt-keywords)