green

uds-psl · Dec 27, 2023 · 6be3a5b · 6be3a5b
1 parent ea1a94b
commit 6be3a5b
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/coq/README.md b/coq/README.md
@@ -11,7 +11,7 @@
 -  Certifying Functions and Sigma Types [certsig.v](certsig.v) 
 -  Linear Arithmetic [la.v](la.v) 
 -  More Types [more.v](more.v) 
-- Indexed Inductives [indind.v](indind.v) 
+-  Indexed Inductives [indind.v](indind.v) 
 -  Extensionality [ext.v](ext.v)
 -  Excluded Middle and Double Negation [xm.v](xm.v)
 -  Provability [provability.v](provability.v)

diff --git a/coq/lwo.v b/coq/lwo.v
@@ -1,4 +1,4 @@
-(*** Least Witness Functions *)
+(*** Least Witness Operators *)
 From Coq Require Import Lia.
 Definition iffT (X Y: Type) : Type := (X -> Y) * (Y -> X).
 Notation "X <=> Y" := (iffT X Y) (at level 95, no associativity).