I am designing a Coq tactic that calls a decision procedure, which answers yes/no, without giving a proof term. When I get yes, I would like to say Ltac that the goal is proved.
Is there a way to do this? For instance, change the goal to True and then use exact I?
I am using Ltac2, but I can use Ltac if it solves the problem.
I've heard about Tactic.change_concl, in Ltac, (https://coq.inria.fr/doc/V8.13.0/api/coq/Tactics/index.html) but I do not know if I can simply change the goal to True; and it is not available in Ltac2.
You basically can't. The point of Coq is that it guarantees proofs that have been checked, down to its own logical principles: a proof written in the language of the calculus of inductive constructions that is well-typed. The tactics are only supposed to help you build such a proof, so anything that accepts the word of a different program as an oracle is outside the philosophy of the system.
Of course, there are workarounds. For instance, you could collect all the results that are proved by an external tool in a database of some sort and then prove with Coq that you final statement is true, under the assumption that all the facts gathered in this database are true. Ltac is not really the right tool for this.
I would suggest looking at the development of the tactics bigenough and near in the math-comp eco system.