Skip to content

GitLab

Commit 572e4e50 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix some typos in comments.

parent 4172cacd
Hide whitespace changes
Inline Side-by-side
Showing with 5 additions and 5 deletions
theories/proofmode/classes.v
View file @ 572e4e50
......@@ -35,13 +35,13 @@ definitions being unfolded (see issue #55).
For binary connectives we have the following instances:
<<
ProgIntoLaterN n P P' IntoLaterN n Q Q'
---------------------------------------------
ProgIntoLaterN n (P /\ Q) (P' /\ Q')
IntoLaterN' n P P' IntoLaterN n Q Q'
------------------------------------------
IntoLaterN' n (P /\ Q) (P' /\ Q')
ProgIntoLaterN n Q Q'
--------------------------------
IntoLaterN' n Q Q'
-------------------------------
IntoLaterN n (P /\ Q) (P /\ 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