Merge pull request #141 from SkySkimmer/ass-lab

Adapt to rocq-prover/rocq#21175 (pass gref to assumptions traversal)

Author: ppedrot

src/declare_translation.ml

@@ -406,10 +406,9 @@ let command_reference ~opaque_access ?(continuation = default_continuation) ?(fu
 
 let command_reference_recursive ~opaque_access ?(continuation = default_continuation) ?(fullname = false) arity gref =
   let gref= Globnames.canonical_gr gref in
-  let label = Names.Label.of_id (Nametab.basename_of_global gref) in
   (* Assumptions doesn't care about the universes *)
   let c, _ = UnivGen.fresh_global_instance (Global.env()) gref in
-  let (direct, graph, _) = Assumptions.traverse opaque_access label c in
+  let (direct, graph, _) = Assumptions.traverse opaque_access gref c in
   let inductive_of_constructor ref =
     let open Globnames in
     let ref= Globnames.canonical_gr ref in