Teach typeclass resolution to make progress on telescopic binders

8afca298 · Ralf Jung · e46551b8 · 8afca298
Commit 8afca298 authored Jun 09, 2018 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 7 additions and 0 deletions

theories/telescopes.v theories/telescopes.v +7 -0

No files found.
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -185,3 +185,10 @@ Proof.
    + rewrite <-(IH p (λ a, Ψ (TargS p a))).
      intros [??]. eauto.
 Qed.
+
+(* Teach typeclass resolution how to make progress on these binders *)
+Typeclasses Opaque tforall texist.
+Hint Extern 1 (tforall _) =>
+  progress cbn [tforall tele_fold tele_bind tele_app] : typeclass_instances.
+Hint Extern 1 (texist _) =>
+  progress cbn [texist tele_fold tele_bind tele_app] : typeclass_instances.