Skip to content

Commit 9e9db0b

Browse files
committed
Adapt to rocq-prover/rocq#19620 (Global.push_context_set no strict argument)
1 parent a379c07 commit 9e9db0b

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/coq_elpi_builtins.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2103,7 +2103,7 @@ Supported attributes:
21032103
| Polymorphic_ind_entry uctx ->
21042104
(Polymorphic_entry uctx, UState.Polymorphic_entry uctx, univ_binders)
21052105
in
2106-
let () = Global.push_context_set ~strict:true uctx in
2106+
let () = Global.push_context_set uctx in
21072107
let mind =
21082108
declare_mutual_inductive_with_eliminations ~primitive_expected ~default_dep_elim me (uentry', ubinders) ind_impls in
21092109
let ind = mind, 0 in

0 commit comments

Comments
 (0)