Target EasyCrypt release 2024.09

[vbgl]

No description provided.

[bgregoir]

Normally, easycrypt should be able to provide this list. I don't know if we should add this dependency.

[vbgl]

Indeed, we could spend a day do develop a tool that may save 5mn every 6 months…

[bgregoir]

It seems that the script $(HOMEEC)/scripts/srctx/keywords < src/ecLexer.mll
print the following:
bytac: assumption, by, done, exact, reflexivity, smt, solve
dangerous: admit, admitted
global: Pr, Self, Top, abbrev, abort, abstract, as, axiom, axiomatized, class, clone, const, declare, dump, end, exit, export, from, goal, hint, import, include, inductive, instance, lemma, local, locate, module, nosmt, notation, of, op, pred, print, proof, prover, qed, realize, remove, rename, require, search, section, theory, timeout, type, why3, with
internal: debug, fail, pragma, time, undo
prog: assert, async, ehoare, elif, else, equiv, exists, for, for, forall, fun, glob, hoare, if, in, is, islossless, let, match, match, phoare, proc, res, return, then, var, while
tactic: algebra, alias, apply, auto, beta, byehoare, byequiv, byphoare, bypr, byupto, call, case, cbv, cfold, change, clear, congr, conseq, delta, eager, ecall, elim, eta, exfalso, exlim, fel, field, fieldeq, fission, fusion, gen, have, idtac, inline, interleave, iota, kill, left, logic, modpath, move, outline, pose, pr_bounded, progress, rcondf, rcondt, replace, rewrite, right, ring, ringeq, rnd, rndsem, rwnormal, seq, sim, simplify, skip, sp, split, splitwhile, subst, suff, swap, symmetry, transitivity, trivial, unroll, weakmem, wlog, wp, zeta
tactical: do, expect, first, last, try