diff options
| author | coqbot-app[bot] | 2020-09-29 21:33:00 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-29 21:33:00 +0000 |
| commit | 2c802aaf74c83274ae922c59081c01bfc267d31b (patch) | |
| tree | 753125fb4bd356669abefbe4838881cf143880bc | |
| parent | a34e213db5c45f0637c4ebf70b84d8020d38000d (diff) | |
| parent | a497cab1da80c148b4c3c815f003e980699dd6d0 (diff) | |
Merge PR #13111: Small document fixes.
Reviewed-by: jfehrle
| -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. |