We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 4ccc472 commit f6daeb4Copy full SHA for f6daeb4
src/run.ml
@@ -1246,8 +1246,7 @@ let declare_mind env sigma params sigs mut_constrs =
1246
let univs, ubinders = Evd.univ_entry ~poly:false sigma in
1247
let uctx = match univs with
1248
| UState.Monomorphic_entry ctx ->
1249
- let () = Global.push_qualities QGraph.Internal (PConstraints.ContextSet.sort_context_set ctx) in (* XXX *)
1250
- let () = Global.push_context_set (PConstraints.ContextSet.univ_context_set ctx) in
+ let () = Global.push_context_set ctx in
1251
Entries.Monomorphic_ind_entry
1252
| UState.Polymorphic_entry uctx -> Entries.Polymorphic_ind_entry uctx
1253
in
0 commit comments