sig
  val evm_compute :
    (Term.constr -> Term.constr -> bool) ->
    Term.constr list -> Proof_type.tactic
  val evm_compute_in :
    (Term.constr -> Term.constr -> bool) ->
    Term.constr list -> Names.identifier -> Proof_type.tactic
end