diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 4 |
2 files changed, 3 insertions, 3 deletions
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)} 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. |