Commit 9c47194e authored by Ralf Jung's avatar Ralf Jung

change some other hints to a more general pattern and typeclass instances

parent 042cbada
...@@ -324,4 +324,4 @@ End sbi_embed. ...@@ -324,4 +324,4 @@ End sbi_embed.
[class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof [class_apply @bi_embed_plainly] shelves the [BiPlainly] premise, making proof
search for the other premises fail. See the proof of [monPred_objectively_plain] search for the other premises fail. See the proof of [monPred_objectively_plain]
for an example where it would fail with a regular [Instance].*) for an example where it would fail with a regular [Instance].*)
Hint Extern 4 (Plain _) => eapply @embed_plain : typeclass_instances. Hint Extern 4 (Plain _) => notypeclasses refine (embed_plain _ _) : typeclass_instances.
...@@ -633,4 +633,4 @@ Hint Immediate plain_persistent : typeclass_instances. ...@@ -633,4 +633,4 @@ Hint Immediate plain_persistent : typeclass_instances.
[class_apply @impl_persistent] shelves the [BiPlainly] premise, making proof [class_apply @impl_persistent] shelves the [BiPlainly] premise, making proof
search for the other premises fail. See the proof of [coreP_persistent] for an search for the other premises fail. See the proof of [coreP_persistent] for an
example where it would fail with a regular [Instance].*) example where it would fail with a regular [Instance].*)
Hint Extern 4 (Persistent (_ _)) => eapply @impl_persistent : typeclass_instances. Hint Extern 4 (Persistent _) => notypeclasses refine (impl_persistent _ _ _ _ _) : 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