From 9995c44df32858624a84a5f87f14a4a24124f84e Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Wed, 30 Sep 2020 02:44:24 +0900
Subject: Type{i} should be Type(i).

---
 doc/sphinx/language/cic.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 768c83150e..f1ed64e52a 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -274,7 +274,7 @@ following rules.
 .. inference:: Prod-Type
 
    \WTEG{T}{s}
-   s \in \{\SProp, \Type{i}\}
+   s \in \{\SProp, \Type(i)\}
    \WTE{\Gamma::(x:T)}{U}{\Type(i)}
    --------------------------------
    \WTEG{∀ x:T,~U}{\Type(i)}
-- 
cgit v1.2.3


From a497cab1da80c148b4c3c815f003e980699dd6d0 Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Wed, 30 Sep 2020 02:50:21 +0900
Subject: Wf.v defines Fix_eq, not fix_eq.

A commit at 2003-03-13 changed the lemma name.
https://github.com/coq/coq/commit/cb1ae314411d78952062e5092804b85d981ad6e1
---
 doc/sphinx/language/coq-library.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index 765373619f..485dfd964d 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -677,7 +677,7 @@ fixpoint equation can be proved.
 
 .. index::
   single: Fix_F (term)
-  single: fix_eq (term)
+  single: Fix_eq (term)
   single: Fix_F_inv (term)
   single: Fix_F_eq (term)
 
@@ -696,7 +696,7 @@ fixpoint equation can be proved.
    forall (x:A) (r:Acc x),
      F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)) = Fix_F x r.
   Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s.
-  Lemma fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y).
+  Lemma Fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y).
   End FixPoint.
   End Well_founded.
 
-- 
cgit v1.2.3