Commit fc191c75 authored by Robbert Krebbers's avatar Robbert Krebbers

More relaxed mode for `MakeMonPredAt`.

This is needed to fix RustBelt-related. Since type classes are no longer
over-eagerly resolved, the `biIndex` now sometimes contains an evar.
parent fb4c6a63
......@@ -6,7 +6,7 @@ Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
(P : monPred I PROP) (𝓟 : PROP) :=
make_monPred_at : P i 𝓟.
Arguments MakeMonPredAt {_ _} _ _%I _%I.
Hint Mode MakeMonPredAt + + - ! - : typeclass_instances.
Hint Mode MakeMonPredAt ! ! - ! - : typeclass_instances.
Class IsBiIndexRel {I : biIndex} (i j : I) := is_bi_index_rel : i j.
Hint Mode IsBiIndexRel + - - : typeclass_instances.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment