From 7a511cd016c4b7add2246527beb34dfae626c9c6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 8 Oct 2025 14:53:31 +0200 Subject: [PATCH] Adapt to rocq-prover/rocq#21175 (pass gref to assumptions traversal) --- src/declare_translation.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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