In my case Tac2env.globals
returns an empty map. Is this normal ?
no
any ideas on what could be wrong ?
IDK show your code
I have this ocaml tactic :
let test_tac () : unit tactic =
let open Ltac2_plugin in
let globals = Tac2env.globals () |> Names.KNmap.bindings in
Feedback.msg_notice
(Pp.str ("count = " ^ string_of_int (List.length globals)));
Tacticals.tclIDTAC
Which I call from Coq :
Lemma test : True.
test_tac.
And it prints count = 0
.
Oh never mind I found the problem
I was calling the tactic test_tac
from a file where I didn't import Ltac2
(I'm in the process of switching from Ltac to Ltac2). After importing Ltac2 the map is longer empty.
Mathis Bouverot-Dupuis has marked this topic as resolved.
you mean Require not Import?
From Ltac2 Require Import Ltac2
to be precise. Sorry for the confusion, the distinction between Import/Require is not clear to me.
Read up on the distinction and now it makes sense that Require
was necessary.
Last updated: Oct 13 2024 at 01:02 UTC