From 572e4e50b57831e1de1d5e3dc0712ff6d9aa9029 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Wed, 22 Mar 2017 00:12:18 +0100 Subject: [PATCH] Fix some typos in comments. --- theories/proofmode/classes.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v index 30c882618..c61a243aa 100644 --- a/theories/proofmode/classes.v +++ b/theories/proofmode/classes.v @@ -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') >> *) -- GitLab