diff --git a/src/declare_translation.ml b/src/declare_translation.ml index ed45236..269b12a 100644 --- a/src/declare_translation.ml +++ b/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