From f25c1d252ad61b4dc4321e3a11f33b1e6d4e3dff Mon Sep 17 00:00:00 2001
From: Timothy Bourke
Date: Sun, 22 Jul 2018 07:43:32 +0200
Subject: Docs: minor typo in W-Ind relative to text

The rule uses s'_j, the text refers to s_j, the latter is simpler in the
absence of any other constraints.
---
 doc/sphinx/language/cic.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 9f932ae78f..b670305389 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -961,7 +961,7 @@ such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;…;I_k :∀ Γ_P ,A_k]`,
 .. inference:: W-Ind
 
    \WFE{Γ_P}
-   (E[Γ_P ] ⊢ A_j : s_j' )_{j=1… k}
+   (E[Γ_P ] ⊢ A_j : s_j )_{j=1… k}
    (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n}
    ------------------------------------------
    \WF{E;\ind{p}{Γ_I}{Γ_C}}{Γ}
-- 
cgit v1.2.3