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