Skip to content

Commit f3ca994

Browse files
authored
Merge pull request #632 from SkySkimmer/abstract-sort-poly
Adapt to rocq-prover/rocq#19073 (univdecl_extensible_qualities)
2 parents 2dbfa59 + 0b39697 commit f3ca994

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/coq_elpi_HOAS.ml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2761,6 +2761,7 @@ let poly_cumul_udecl_variance_of_options state options =
27612761
let open UState in
27622762
state, true, true,
27632763
{ univdecl_qualities = [];
2764+
univdecl_extensible_qualities = false;
27642765
univdecl_extensible_instance;
27652766
univdecl_extensible_constraints;
27662767
univdecl_constraints;
@@ -2772,6 +2773,7 @@ let poly_cumul_udecl_variance_of_options state options =
27722773
let open UState in
27732774
state, true, false,
27742775
{ univdecl_qualities = [];
2776+
univdecl_extensible_qualities = false;
27752777
univdecl_extensible_instance;
27762778
univdecl_extensible_constraints;
27772779
univdecl_constraints;

0 commit comments

Comments
 (0)