Skip to content

Commit

Permalink
Adapt to coq/coq#17283 (More careful handling of possibly universe po…
Browse files Browse the repository at this point in the history
…lymorphic globrefs)
  • Loading branch information
SkySkimmer committed Feb 24, 2023
1 parent ca56b5d commit 2b015c1
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/declare_translation.ml
Original file line number Diff line number Diff line change
Expand Up @@ -394,10 +394,10 @@ let command_reference ?(continuation = default_continuation) ?(fullname = false)
in ()

let command_reference_recursive ?(continuation = default_continuation) ?(fullname = false) arity gref =
let open Globnames in
let gref= Globnames.canonical_gr gref in
let label = Names.Label.of_id (Nametab.basename_of_global gref) in
let c = printable_constr_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 label c in
let inductive_of_constructor ref =
let open Globnames in
Expand Down

0 comments on commit 2b015c1

Please sign in to comment.