[petanque] Use lighter goal query on run_tac

This avoids printing and unfreezing, which is no question a
performance gain.

fleche/info.ml

@@ -149,6 +149,14 @@ module O = Make (Offset)
 
 (* Related to goal request *)
 module Goals = struct
+  let get_goals_unit ~st =
+    let ppx _env _sigma _x = () in
+    Coq.State.lemmas ~st |> Option.map (Coq.Goals.reify ~ppx)
+
+  let get_goals ~st =
+    let ppx env sigma x = (env, sigma, x) in
+    Coq.State.lemmas ~st |> Option.map (Coq.Goals.reify ~ppx)
+
   let pr_goal ~token st =
     let ppx env sigma x =
       let { Coq.Protect.E.r; feedback } =

fleche/info.mli

@@ -52,6 +52,16 @@ module O : S with module P := Offset
 
 (** We move towards a more modular design here, for preprocessing *)
 module Goals : sig
+  val get_goals_unit :
+    st:Coq.State.t -> (unit Coq.Goals.reified_goal, Pp.t) Coq.Goals.goals option
+
+  val get_goals :
+       st:Coq.State.t
+    -> ( (Environ.env * Evd.evar_map * EConstr.t) Coq.Goals.reified_goal
+       , Pp.t )
+       Coq.Goals.goals
+       option
+
   val goals :
        token:Coq.Limits.Token.t
     -> st:Coq.State.t

petanque/agent.ml

@@ -167,8 +167,8 @@ let parse_and_execute_in ~token ~loc tac st =
   match ast with
   | Some ast -> (
     let open Coq.Protect.E.O in
-    let* st = Fleche.Memo.Interp.eval ~token (st, ast) in
-    let+ goals = Fleche.Info.Goals.goals ~token ~st in
+    let+ st = Fleche.Memo.Interp.eval ~token (st, ast) in
+    let goals = Fleche.Info.Goals.get_goals_unit ~st in
     match goals with
     | None -> Run_result.Proof_finished st
     | Some goals when proof_finished goals -> Run_result.Proof_finished st