From 69e852924a9419eeff5cf5875f649fd898d2ba07 Mon Sep 17 00:00:00 2001
From: Joachim Breitner
Date: Sun, 16 Sep 2018 21:33:13 +0200
Subject: Mising prime in the subtyping rules

---
 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 9c2ba50362..ac0f0f8ea6 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -640,7 +640,7 @@ a *subtyping* relation inductively defined by:
    respectively then
 
    .. math::
-      E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t~w_1' … w_m'
+      E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t'~w_1' … w_m'
 
    (notice that :math:`t` and :math:`t'` are both
    fully applied, i.e., they have a sort as a type) if
-- 
cgit v1.2.3