Skip to content

Commit 3f23dcc

Browse files
authored
Merge pull request #68 from herbelin/master+adapt-coq-pr14692-slight-simplification-UContext
Adapting to Coq PR #14692: UContext now includes the names by default
2 parents 1d9409b + 4db048b commit 3f23dcc

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/debug.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -194,7 +194,7 @@ let debug_mutual_inductive_entry =
194194
match entry.mind_entry_universes with
195195
| Monomorphic_entry ux ->
196196
Univ.pr_universe_context_set UnivNames.(pr_with_global_universes empty_binders) ux
197-
| Polymorphic_entry (_,ux) ->
197+
| Polymorphic_entry ux ->
198198
Univ.pr_universe_context UnivNames.(pr_with_global_universes empty_binders) ux
199199
in
200200
let mind_entry_cumul_pp = bool (Option.has_some entry.mind_entry_variance) in

0 commit comments

Comments
 (0)