Commit aaf62d5e authored by Robbert Krebbers's avatar Robbert Krebbers

Fix some comments.

parent d23ae90d
......@@ -84,7 +84,7 @@ Hint Mode FromAlways + - ! - : typeclass_instances.
progress, i.e. its instances should actually strip a later.
The point of using the auxilary class [IntoLaterN'] is to ensure that the
default instance is not applied deeply in the term, which may cause in too many
default instance is not applied deeply in the term, which may result in too many
definitions being unfolded (see issue #55).
For binary connectives we have the following instances:
......@@ -97,7 +97,7 @@ IntoLaterN' n P P' IntoLaterN n Q Q'
IntoLaterN' n Q Q'
-------------------------------
IntoLaterN n (P /\ Q) (P /\ Q')
IntoLaterN' n (P /\ Q) (P /\ Q')
>>
*)
Class IntoLaterN {M} (n : nat) (P Q : uPred M) := into_laterN : P ^n Q.
......
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