Tutorial on the new proof engine for ML tactic writers ====================================================== Starting from Coq 8.5, a new proof engine has been introduced, replacing the old meta-based engine which had a lot of drawbacks, ranging from expressivity to soundness, the major one being that the type of tactics was transparent. This was pervasively abused and made virtually impossible to tweak the implementation of the engine. The old engine is deprecated and is slowly getting removed from the source code. The new engine relies on a monadic API defined in the `Proofview` module. Helper functions and higher-level operations are defined in the `Tacmach` and `Tacticals` modules, and end-user tactics are defined amongst other in the `Tactics` module. At the root of the engine is a representation of proofs as partial terms that can contain typed holes, called evars, short for *existential variable*. An evar is essentially defined by its context and return type, that we will write `?e : [Γ ⊢ _ : A]`. An evar `?e` must be applied to a substitution `σ` of type `Γ` (i.e. a list of terms) to produce a term of type `A`, which is done by applying `EConstr.mkEvar`, and which we will write `?e{σ}`. The engine monad features a notion of global state called `evar_map`, defined in the `Evd` module, which is the structure containing the incremental refinement of evars. `Evd` is a low-level API and its use is discouraged in favour of the `Evarutil` module which provides more abstract primitives. In addition to this state, the monad also features a goal state, that is an ordered list of current holes to be filled. While these holes are referred to as goals at a high-enough level, they are actually no more than evars. The API provided to deal with these holes can be found in the `Proofview.Goal` module. Tactics are naturally operating on several goals at once, so that it is usual to use the `Proofview.Goal.enter` function and its variants to dispatch a tactic to each of the goals under focus. Primitive tactics by te…